diff options
Diffstat (limited to 'Source/VCGeneration/VC.cs')
| -rw-r--r-- | Source/VCGeneration/VC.cs | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 373b685a..18417830 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1403,6 +1403,12 @@ namespace VC { ConvertCFG2DAG(impl);
+ if (CommandLineOptions.Clo.DoPredication) {
+ DesugarCalls(impl);
+ BlockPredicator.Predicate(program, impl);
+ impl.ComputePredecessorsForBlocks();
+ }
+
SmokeTester smoke_tester = null;
if (CommandLineOptions.Clo.SoundnessSmokeTest) {
smoke_tester = new SmokeTester(this, impl, program, callback);
@@ -1968,6 +1974,26 @@ namespace VC { #endregion
}
+ public void DesugarCalls(Implementation impl) {
+ foreach (Block block in impl.Blocks) {
+ CmdSeq newCmds = new CmdSeq();
+ foreach (Cmd cmd in block.Cmds) {
+ SugaredCmd sugaredCmd = cmd as SugaredCmd;
+ if (sugaredCmd != null) {
+ StateCmd stateCmd = sugaredCmd.Desugaring as StateCmd;
+ foreach (Variable v in stateCmd.Locals) {
+ impl.LocVars.Add(v);
+ }
+ newCmds.AddRange(stateCmd.Cmds);
+ }
+ else {
+ newCmds.Add(cmd);
+ }
+ }
+ block.Cmds = newCmds;
+ }
+ }
+
public Hashtable/*TransferCmd->ReturnCmd*/ PassifyImpl(Implementation impl, out ModelViewInfo mvInfo)
{
Contract.Requires(impl != null);
|