Merge pull request #7606 from qinheping/object_bits_in_synthesizer

SYNTHESIZER: Add an option to specify object bits in synthesizer

Author: tautschnig

doc/man/goto-synthesizer.1

@@ -18,13 +18,17 @@ resulting program as GOTO binary on disk.
 .SH OPTIONS
 .TP
 \fB\-loop\-contracts\-no\-unwind\fR
-Do not unwind transformed loops after applying the synthesized loop contracts.
+do not unwind transformed loops after applying the synthesized loop contracts
 .TP
 \fB\-\-dump\-loop\-contracts
-Dump the synthesized loop contracts as JSON.
+dump the synthesized loop contracts as JSON
 .TP
 \fB\-\-json-\output\fR \fIfile\fR
-Specify the output destination of the loop-contracts JSON.
+specify the output destination of the loop-contracts JSON
+.SS "Backend options:"
+.TP
+\fB\-\-object\-bits\fR n
+number of bits used for object addresses
 .SS "User-interface options:"
 .TP
 \fB\-\-xml\-ui\fR

regression/goto-synthesizer/address_space_size_limit/main.c

@@ -0,0 +1,20 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main()
+{
+  int i;
+  char *a;
+  char *b;
+  char *c;
+  a = (char *)malloc(1);
+  b = (char *)malloc(1);
+  c = (char *)malloc(1);
+  for(i = 0; i < 5; ++i)
+  {
+    *a = 0;
+    *b = 0;
+    *c = 0;
+  }
+  assert(*c + *b + *c == 1);
+}

regression/goto-synthesizer/address_space_size_limit/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check _ --object-bits 1
+too many addressed objects
+^EXIT=6$
+^SIGNAL=0$
+--
+Check if the synthesizer can correctly set object bits when calling CBMC.

regression/goto-synthesizer/chain.sh

@@ -48,7 +48,7 @@ echo "Running goto-synthesizer: "
 if echo $args_synthesizer | grep -q -- "--dump-loop-contracts" ; then
   $goto_synthesizer ${args_synthesizer} "${name}-mod.gb"
 else
-  $goto_synthesizer "${name}-mod.gb" "${name}-mod-2.gb"
+  $goto_synthesizer ${args_synthesizer} "${name}-mod.gb" "${name}-mod-2.gb"
   echo "Running CBMC: "
   $cbmc "${name}-mod-2.gb"
 fi

src/goto-synthesizer/goto_synthesizer_parse_options.cpp

@@ -8,7 +8,6 @@ Author: Qinheping Hu
 
 #include "goto_synthesizer_parse_options.h"
 
-#include <util/config.h>
 #include <util/exit_codes.h>
 #include <util/version.h>
 
@@ -196,6 +195,9 @@ void goto_synthesizer_parse_optionst::help()
     HELP_DUMP_LOOP_CONTRACTS
     HELP_LOOP_CONTRACTS_NO_UNWIND
     "\n"
+    "Backend options:\n"
+    HELP_CONFIG_BACKEND
+    "\n"
     "Other options:\n"
     " --version                    show version and exit\n"
     " --xml-ui                     use XML-formatted output\n"

src/goto-synthesizer/goto_synthesizer_parse_options.h

@@ -9,6 +9,7 @@ Author: Qinheping Hu
 #ifndef CPROVER_GOTO_SYNTHESIZER_GOTO_SYNTHESIZER_PARSE_OPTIONS_H
 #define CPROVER_GOTO_SYNTHESIZER_GOTO_SYNTHESIZER_PARSE_OPTIONS_H
 
+#include <util/config.h>
 #include <util/parse_options.h>
 
 #include <goto-programs/goto_model.h>
@@ -21,6 +22,7 @@ Author: Qinheping Hu
 #define GOTO_SYNTHESIZER_OPTIONS \
   OPT_DUMP_LOOP_CONTRACTS \
   "(" FLAG_LOOP_CONTRACTS_NO_UNWIND ")" \
+  OPT_CONFIG_BACKEND \
   "(verbosity):(version)(xml-ui)(json-ui)" \
   // empty last line