replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

There is no need for argc and argv to be new, as long types match 

Consider the following unlikely sequence of events:

$ cat ~/tmp/can-delete/main.c
int main (int argc, char **argv) {
  return 0;
}
$ goto-cc main.c -o main.goto
$ cbmc main.goto --function main
CBMC version 5.11 (cbmc-5.11-881-gd52cd0d1e-dirty) 64-bit x86_64 linux
Reading GOTO program from file
Reading: /home/martin/tmp/can-delete/main.goto
failed to insert argc symbol
SUPPORT FUNCTION GENERATION ERROR

argc and argv both exist and it is fine to re-use them.  If the
addition fails it will throw an exception, the .second bool is only
false in the case they already exist which is likely harmless.
This commit is contained in:
martin 2019-03-14 16:32:14 +00:00
parent 1c309e1b23
commit 2bee6b195f
1 changed files with 8 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
src/ansi-c/ansi_c_entry_point.cpp
View File

@ -268,10 +268,12 @@ bool generate_ansi_c_start_function(
argc_symbol.is_lvalue = true;
argc_symbol.mode = ID_C;
if(!symbol_table.insert(std::move(argc_symbol)).second)
auto r = symbol_table.insert(argc_symbol);
if(!r.second && r.first != argc_symbol)
{
messaget message(message_handler);
message.error() << "failed to insert argc symbol" << messaget::eom;
message.error() << "argc already exists but is not usable"
<< messaget::eom;
return true;
}
}
@ -295,10 +297,12 @@ bool generate_ansi_c_start_function(
argv_symbol.is_lvalue = true;
argv_symbol.mode = ID_C;
if(!symbol_table.insert(std::move(argv_symbol)).second)
auto r = symbol_table.insert(argv_symbol);
if(!r.second && r.first != argv_symbol)
{
messaget message(message_handler);
message.error() << "failed to insert argv symbol" << messaget::eom;
message.error() << "argv already exists but is not usable"
<< messaget::eom;
return true;
}
}