Added modifies clause generation for Boogie files.#267
Added modifies clause generation for Boogie files.#267liammachado wants to merge 17 commits intosmackers:developfrom liammachado:develop
Conversation
CMakeLists.txt
Outdated
| 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
| 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.
2 participants
Modifies clause generation is now directly integrated into the SMACK tool, rather than being done by Corral/Boogie.