Merge branch 'master' of github.com:diffblue/cbmc

Author: Daniel Kroening

appveyor.yml

@@ -75,6 +75,10 @@ test_script:
     cat goto-instrument-typedef/chain.sh || true
 
     rem HACK disable failing tests
+    rmdir /s /q ansi-c\arch_flags_mcpu_bad
+    rmdir /s /q ansi-c\arch_flags_mcpu_good
+    rmdir /s /q ansi-c\arch_flags_mthumb_bad
+    rmdir /s /q ansi-c\arch_flags_mthumb_good
     rmdir /s /q ansi-c\Forward_Declaration2
     rmdir /s /q ansi-c\Incomplete_Type1
     rmdir /s /q ansi-c\Union_Padding1

regression/Makefile

@@ -12,3 +12,10 @@ DIRS = ansi-c \
 
 test:
 	$(foreach var,$(DIRS), $(MAKE) -C $(var) test || exit 1;)
+
+clean:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			$(MAKE) -C "$$dir" clean; \
+		fi; \
+	done;

regression/ansi-c/arch_flags_mcpu_bad/object.intel

@@ -0,0 +1 @@
+int foo() { return 3; }

regression/ansi-c/arch_flags_mcpu_bad/preproc.i

@@ -0,0 +1 @@
+int bar(){ return 9; }

regression/ansi-c/arch_flags_mcpu_bad/source.c

@@ -0,0 +1,20 @@
+CORE
+preproc.i
+-mcpu=cortex-a15 -o linked-object.gb object.intel
+^EXIT=(64|1)$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
+--
+This tests the -mcpu=cortex=a15 flag that should activate ARM-32 mode.
+The object file 'object.intel' was compiled from 'source.c' with goto-cc
+on a 64-bit platform:
+
+  goto-cc -c source.c
+
+preproc.i is already pre-processed so that it can be linked in without
+needing to invoke a pre-processor from a cross-compile toolchain on your
+local machine. Linking it together with the Intel object file, while
+passing -mcpu=cortex-a15 on the command line, should fail because
+-mcpu=cortex-a15 implies that we're trying to make an ARM executable.

regression/ansi-c/arch_flags_mcpu_bad/test.desc

@@ -0,0 +1 @@
+int foo() { return 3; }

regression/ansi-c/arch_flags_mcpu_good/object.arm

@@ -0,0 +1 @@
+int bar(){ return 9; }

regression/ansi-c/arch_flags_mcpu_good/preproc.i

@@ -0,0 +1,20 @@
+CORE
+preproc.i
+-mcpu=cortex-a15 -o linked-object.gb object.arm
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
+--
+This tests the -mcpu=cortex-a15 flag that should activate ARM-32 mode.
+The object file 'object.arm' was compiled from 'source.c' with goto-cc
+along with an ARM cross-compiler on a 64-bit platform with the following
+command line:
+
+  goto-cc --native-compiler=arm-none-eabi-gcc -mcpu=cortex-a15 -c source.c
+
+preproc.i is already pre-processed so that it can be linked in without
+needing to invoke a pre-processor from a cross-compile toolchain on your
+local machine. Linking it together with the ARM object file, while
+passing -mcpu=cortex-a15 on the command line, should succeed.

regression/ansi-c/arch_flags_mcpu_good/source.c

@@ -0,0 +1 @@
+int foo() { return 3; }

regression/ansi-c/arch_flags_mcpu_good/test.desc

@@ -0,0 +1 @@
+int bar(){ return 9; }

regression/ansi-c/arch_flags_mthumb_bad/object.intel

@@ -0,0 +1,20 @@
+CORE
+preproc.i
+-mthumb -o linked-object.gb object.intel
+^EXIT=(64|1)$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
+--
+This tests the -mthumb flag that should activate ARM-32 mode. The object
+file 'object.intel' was compiled from 'source.c' with goto-cc on a
+64-bit platform:
+
+  goto-cc -c source.c
+
+preproc.i is already pre-processed so that it can be linked in without
+needing to invoke a pre-processor from a cross-compile toolchain on your
+local machine. Linking it together with the Intel object file, while
+passing -mthumb on the command line, should fail because -mthumb implies
+that we're trying to make an ARM executable.

regression/ansi-c/arch_flags_mthumb_bad/preproc.i

@@ -0,0 +1 @@
+int foo() { return 3; }

regression/ansi-c/arch_flags_mthumb_bad/source.c

@@ -0,0 +1 @@
+int bar(){ return 9; }

regression/ansi-c/arch_flags_mthumb_bad/test.desc

@@ -0,0 +1,20 @@
+CORE
+preproc.i
+-mthumb -o linked-object.gb object.arm
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
+--
+This tests the -mthumb flag that should activate ARM-32 mode. The object
+file 'object.arm' was compiled from 'source.c' with goto-cc along with
+an ARM cross-compiler on a 64-bit platform with the following command
+line:
+
+  goto-cc --native-compiler=arm-none-eabi-gcc -mthumb -c source.c
+
+preproc.i is already pre-processed so that it can be linked in without
+needing to invoke a pre-processor from a cross-compile toolchain on your
+local machine. Linking it together with the ARM object file, while
+passing -mthumb on the command line, should succeed.

regression/ansi-c/arch_flags_mthumb_good/object.arm

@@ -0,0 +1,12 @@
+char buffer[2];
+int length = 2;
+
+void func(void* buf, int len)
+{
+  while( len-- )
+    *(char *)buf++;
+}
+
+void main(){
+  func(buffer,length);
+}

regression/ansi-c/arch_flags_mthumb_good/preproc.i

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/ansi-c/arch_flags_mthumb_good/source.c

@@ -0,0 +1,12 @@
+char buffer[2];
+int length = 2;
+
+void func(void* buf, int len)
+{
+  while( len-- )
+    *(char *)buf++;
+}
+
+void main(){
+  func(buffer,length);
+}

regression/ansi-c/arch_flags_mthumb_good/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --no-simplify --unwind 3
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/void_pointer1/main.c

@@ -4,7 +4,7 @@ int main()
   signed int i;
   signed int j;
   i = 0;
-   if(!(i >= 2))
+  if(!(i >= 2))
   {
     j = j + 1;
     i = i + 1;

regression/cbmc/void_pointer1/test.desc

@@ -11,6 +11,9 @@ Date: August 2013
 
 #include <cassert>
 
+#include <util/json.h>
+#include <util/json_expr.h>
+
 #include "goto_rw.h"
 
 #include "dependence_graph.h"
@@ -347,6 +350,46 @@ void dep_graph_domaint::output(
 
 /*******************************************************************\
 
+Function: dep_graph_domaint::output_json
+
+  Inputs: The abstract interpreter and the namespace.
+
+ Outputs: The domain, formatted as a JSON object.
+
+ Purpose: Outputs the current value of the domain.
+
+\*******************************************************************/
+
+jsont dep_graph_domaint::output_json(
+  const ai_baset &ai,
+  const namespacet &ns) const
+{
+  json_arrayt graph;
+
+  for(const auto &cd : control_deps)
+  {
+    json_objectt &link=graph.push_back().make_object();
+    link["locationNumber"]=
+      json_numbert(std::to_string(cd->location_number));
+    link["sourceLocation"]=json(cd->source_location);
+    link["type"]=json_stringt("control");
+  }
+
+  for(const auto &dd : data_deps)
+  {
+    json_objectt &link=graph.push_back().make_object();
+    link["locationNumber"]=
+      json_numbert(std::to_string(dd->location_number));
+    link["sourceLocation"]=json(dd->source_location);
+      json_stringt(dd->source_location.as_string());
+    link["type"]=json_stringt("data");
+  }
+
+  return graph;
+}
+
+/*******************************************************************\
+
 Function: dependence_grapht::add_dep
 
   Inputs:

regression/cbmc/void_pointer2/main.c

@@ -87,7 +87,11 @@ class dep_graph_domaint:public ai_domain_baset
     const ai_baset &ai,
     const namespacet &ns) const final;
 
-  void make_top() final
+  jsont output_json(
+    const ai_baset &ai,
+    const namespacet &ns) const override;
+
+  void make_top() final override
   {
     assert(node_id!=std::numeric_limits<node_indext>::max());
 

regression/cbmc/void_pointer2/test.desc

@@ -1238,7 +1238,8 @@ void goto_checkt::bounds_check(
     plus_exprt effective_offset(ode.offset(), pointer_offset(pointer));
 
     assert(effective_offset.op0().type()==effective_offset.op1().type());
-    assert(effective_offset.type()==size.type());
+    if(effective_offset.type()!=size.type())
+      size.make_typecast(effective_offset.type());
 
     binary_relation_exprt inequality(effective_offset, ID_lt, size);
 

regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c

@@ -149,6 +149,7 @@ void rw_range_sett::get_objects_complex(
 
   range_spect sub_size=
     to_range_spect(pointer_offset_bits(op.type().subtype(), ns));
+  assert(sub_size>0);
   range_spect offset=
     (range_start==-1 || expr.id()==ID_complex_real) ? 0 : sub_size;
 

src/analyses/dependence_graph.cpp

@@ -157,8 +157,8 @@ bool interval_domaint::merge(
   for(int_mapt::iterator it=int_map.begin();
       it!=int_map.end(); ) // no it++
   {
-    //search for the variable that needs to be merged
-    //containers have different size and variable order
+    // search for the variable that needs to be merged
+    // containers have different size and variable order
     const int_mapt::const_iterator b_it=b.int_map.find(it->first);
     if(b_it==b.int_map.end())
     {

src/analyses/dependence_graph.h

@@ -16,7 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/base_type.h>
 #include <util/std_types.h>
 
-#include <ansi-c/c_types.h>
+#include <util/c_types.h>
 #include <langapi/language_util.h>
 
 #include "invariant_set.h"

src/analyses/goto_check.cpp

@@ -13,7 +13,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_code.h>
 #include <util/expr_util.h>
 
-#include <ansi-c/c_types.h>
+#include <util/c_types.h>
 #include <langapi/language_util.h>
 
 #include "local_bitvector_analysis.h"

src/analyses/goto_rw.cpp

@@ -14,7 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_code.h>
 #include <util/expr_util.h>
 
-#include <ansi-c/c_types.h>
+#include <util/c_types.h>
 #include <langapi/language_util.h>
 
 #endif

src/analyses/interval_domain.cpp

@@ -13,7 +13,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_expr.h>
 #include <util/std_code.h>
 
-#include <ansi-c/c_types.h>
+#include <util/c_types.h>
 #include <langapi/language_util.h>
 
 #include "local_may_alias.h"

src/analyses/invariant_set.cpp

@@ -24,7 +24,6 @@ SRC = anonymous_member.cpp \
       c_typecheck_initializer.cpp \
       c_typecheck_type.cpp \
       c_typecheck_typecast.cpp \
-      c_types.cpp \
       cprover_library.cpp \
       designator.cpp \
       expr2c.cpp \

src/analyses/local_bitvector_analysis.cpp

@@ -8,6 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <cassert>
 
+#include <util/c_types.h>
 #include <util/namespace.h>
 #include <util/simplify_expr.h>
 #include <util/config.h>

src/analyses/local_cfg.cpp

@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/message.h>
 
-#include "c_types.h"
 #include "c_qualifiers.h"
 #include "c_storage_spec.h"
 

src/analyses/local_may_alias.cpp

@@ -17,7 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/cprover_prefix.h>
 #include <util/prefix.h>
 
-#include <ansi-c/c_types.h>
+#include <util/c_types.h>
 #include <ansi-c/string_constant.h>
 
 #include <goto-programs/goto_functions.h>

src/ansi-c/Makefile

@@ -10,6 +10,7 @@ Author: DiffBlue Limited. All rights reserved.
 #include <sstream>
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/fresh_symbol.h>
 #include <util/std_types.h>
 #include <util/std_code.h>
@@ -20,7 +21,6 @@ Author: DiffBlue Limited. All rights reserved.
 
 #include <linking/zero_initializer.h>
 
-#include <ansi-c/c_types.h>
 #include <ansi-c/string_constant.h>
 
 #include <goto-programs/goto_functions.h>

src/ansi-c/ansi_c_convert_type.cpp

@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <fstream>
 
+#include <util/c_types.h>
 #include <util/config.h>
 #include <util/message.h>
 #include <util/tempfile.h>
@@ -29,7 +30,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_types.h>
 #include <util/prefix.h>
 
-#include "c_types.h"
 #include "c_preprocess.h"
 
 #define GCC_DEFINES_16 \

src/ansi-c/ansi_c_convert_type.h

@@ -6,14 +6,14 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
+#include <util/c_types.h>
 #include <util/config.h>
 #include <util/arith_tools.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 
 #include "c_sizeof.h"
 #include "c_typecast.h"
-#include "c_types.h"
 
 /*******************************************************************\