diff options
author | Akash Lal <akashl@microsoft.com> | 2015-05-07 15:18:11 +0530 |
---|---|---|
committer | Akash Lal <akashl@microsoft.com> | 2015-05-07 15:18:11 +0530 |
commit | 0234f41446ed24b0327497aaedf0caafcc0afb0c (patch) | |
tree | 1eb7b53702f3939396819561d8b175a442955af2 /Source/VCGeneration | |
parent | c09814e1ae44a0bee53abb6e8e65b79c1da03d9e (diff) |
Fix for secureVCGen
Diffstat (limited to 'Source/VCGeneration')
-rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 6f8d3668..e88eb55e 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -2609,6 +2609,9 @@ namespace VC { if(impl.LocVars.Any(v => isVisible(v)))
throw new InvalidProgramForSecureVc("SecureVc: Visible Local variables not allowed");
+ // Desugar procedure calls
+ DesugarCalls(impl);
+
// Gather spec, remove existing ensures
var secureAsserts = new List<AssertCmd>();
var logicalAsserts = new List<AssertCmd>();
|