Added modifies clause generation for Boogie files. #267
Conversation
CMakeLists.txt
Outdated
| @@ -175,6 +175,7 @@ add_library(smackTranslator STATIC | |||
| include/smack/MemorySafetyChecker.h | |||
| include/smack/SignedIntegerOverflowChecker.h | |||
| include/smack/SplitAggregateLoadStore.h | |||
| include/smack/GenModifies.h | |||
There was a problem hiding this comment.
I think that naming this file ModAnalysis would be better. So update its name.
include/smack/GenModifies.h
Outdated
| // | ||
| // This file is distributed under the MIT License. See LICENSE for details. | ||
| // | ||
| #ifndef MODS_H |
There was a problem hiding this comment.
Change the file name to ModAnalysis.h.
Also, this should be #ifndef MODANALYSIS_H to make it consistent with other files.
include/smack/GenModifies.h
Outdated
| // This file is distributed under the MIT License. See LICENSE for details. | ||
| // | ||
| #ifndef MODS_H | ||
| #define MODS_H |
There was a problem hiding this comment.
See above comment. Change this to MODANALYSIS_H
share/smack/top.py
Outdated
| @@ -512,7 +512,7 @@ def verify_bpl(args): | |||
| elif args.verifier == 'boogie' or args.modular: | |||
| command = ["boogie"] | |||
| command += [args.bpl_file] | |||
| command += ["/nologo", "/noinfer", "/doModSetAnalysis"] | |||
| #command += ["/nologo", "/noinfer", "/doModSetAnalysis"] | |||
There was a problem hiding this comment.
Don't comment this whole line out. Just remove /doModSetAnalysis
lib/smack/GenModifies.cpp
Outdated
|
|
||
| void GenModifies::genUserCodeModifies(Program *program, const std::set<std::string> &bplGlobals) { | ||
| genSCCs(program); | ||
|
|
There was a problem hiding this comment.
Remove this empty line, it is not needed here.
lib/smack/GenModifies.cpp
Outdated
| std::string modClause = getBplGlobalsModifiesClause(bplGlobals); | ||
|
|
||
| fixPrelude(program, modClause); | ||
|
|
There was a problem hiding this comment.
Remove this empty line, it is not needed here.
lib/smack/GenModifies.cpp
Outdated
| if (isa<CodeDecl>(decl)) { | ||
| if (PROC_DECL.match(decl->getName()) && !MOD_CL.match(decl->getName())) { | ||
| std::string newStr = PROC_DECL.sub("\\1", decl->getName()) + modClause + PROC_DECL.sub("\\3", decl->getName()); | ||
|
|
There was a problem hiding this comment.
Remove this empty line, it is not needed here.
lib/smack/GenModifies.cpp
Outdated
|
|
||
| void GenModifies::fixPrelude(Program *program, const std::string &modClause) { | ||
| std::string searchStr = "procedure $global_allocations()\n"; | ||
|
|
There was a problem hiding this comment.
Remove this empty line, it is not needed here.
lib/smack/GenModifies.cpp
Outdated
| std::string searchStr = "procedure $global_allocations()\n"; | ||
|
|
||
| std::string &prelude = program->getPrelude(); | ||
|
|
There was a problem hiding this comment.
Remove this empty line, it is not needed here.
lib/smack/GenModifies.cpp
Outdated
| if (pos != std::string::npos) { | ||
| std::string str1 = prelude.substr(0, pos + searchStr.size()); | ||
| std::string str2 = prelude.substr(pos + searchStr.size()); | ||
|
|
There was a problem hiding this comment.
Remove this empty line, it is not needed here.
…ry-safety regtests to fail. The modifies pass was not handling the prelude section of Boogie files. When the --memory-safety option is specified, this prelude section contains a procedure called $global_allocations which modifies some variables. Additionally, the modifies pass only adds modifies clauses to SMACK-generated procedures that do not already have one, which does not cover the $malloc procedure when the --memory-safety option is set. This is directly changed in smack.c.
…fety option is not specified.
…t have been there.
Modifies clause generation is now directly integrated into the SMACK tool, rather than being done by Corral/Boogie.