Corrections for 675

regression/.gitignore

@@ -0,0 +1 @@
+tests.log

regression/cbmc-java/assume1/Assume1.java

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class Assume1
+{
+  static void foo(int x)
+  {
+    CProver.assume(x>3);
+    assert x>0;
+  }
+}

regression/cbmc-java/assume1/test.desc

@@ -0,0 +1,8 @@
+CORE
+Assume1.class
+--function Assume1.foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/assume2/Assume2.java

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class Assume2
+{
+  static void foo(int x)
+  {
+    CProver.assume(x>3);    
+    assert x>4;
+  }
+}

regression/cbmc-java/assume2/test.desc

@@ -0,0 +1,8 @@
+CORE
+Assume2.class
+--function Assume2.foo
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/assume3/Assume3.java

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class Assume3
+{
+  public static void main(String[] args)
+  {
+    CProver.assume(false);
+    assert false;
+  }
+}

regression/cbmc-java/assume3/test.desc

@@ -0,0 +1,8 @@
+CORE
+Assume3.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/covered1/covered1.java

@@ -0,0 +1,37 @@
+public class covered1
+{
+  // this is a variable
+  int x=1;
+  //these are two, one line off the first
+  int y=2;
+  int z=3;
+  //this is part of static init
+  static int z0=0;
+
+  //another non-static
+  int a;
+  int b;
+  static boolean odd;
+
+  static
+  {
+    odd=(z0+1)%2==0;
+  }
+
+  covered1(int a, int b)
+  {
+    this.a=a*b;
+    this.b=a+b;
+    if(this.a==a)
+      z0++;
+    else
+      odd=!odd;
+  }
+  // at the back
+  int z1=2;
+  int z2=3;
+  int z3=4;
+  //
+  static int z4=5;
+  int z5=5;
+}

regression/cbmc-java/covered1/test.desc

@@ -0,0 +1,19 @@
+CORE
+covered1.class
+--cover location --json-ui --show-properties
+^EXIT=0$
+^SIGNAL=0$
+.*\"coveredLines\": \"22\",$
+.*\"coveredLines\": \"4,6,7,23-25,31-33,36\",$
+.*\"coveredLines\": \"26\",$
+.*\"coveredLines\": \"28\",$
+.*\"coveredLines\": \"28\",$
+.*\"coveredLines\": \"28\",$
+.*\"coveredLines\": \"28\",$
+.*\"coveredLines\": \"29\",$
+.*\"coveredLines\": \"9,18\",$
+.*\"coveredLines\": \"18\",$
+.*\"coveredLines\": \"18\",$
+.*\"coveredLines\": \"18,35\",$
+--
+^warning: ignoring

scripts/bash-autocomplete/.gitignore

@@ -0,0 +1 @@
+cbmc.sh

scripts/bash-autocomplete/Readme.md

@@ -0,0 +1,31 @@
+# CBMC Autocomplete Scripts for Bash
+This directory contains an autocomplete script for bash.
+## Installation
+1. Compile cbmc and
+
+2. `cd scripts/bash-autocomplete`
+
+3.  `./extract-switches.sh`
+
+4. Put the following at the end of you in your `~/.bashrc`, with the directories adapted to your directory structure:
+    ```bash
+    cbmcautocomplete=~/diffblue/cbmc/scripts/bash-autocomplete/cbmc.sh
+    if [ -f $cbmcautocomplete ]; then
+      . $cbmcautocomplete
+    fi
+    ```
+## Usage
+As with the usual autocomplete in bash, start typing a switch to complete it, for example:
+```
+cbmc --clas<TAB>
+```
+will complete to
+```
+cbmc --classpath
+```
+
+## Features implemented
+
+* Completing all switches
+* Completing values for `--cover`, `--mm` and `--arch`
+* When completing a name of a file to analyze, only files with supported extensions are shown.

scripts/bash-autocomplete/cbmc.sh.template

@@ -0,0 +1,43 @@
+#!/bin/bash
+_cbmc_autocomplete()
+{
+  #list of all switches cbmc has. IMPORTANT: in the template file, this variable must be defined on line 5.
+  local switches=""
+  #word on which the cursor is
+  local cur=${COMP_WORDS[COMP_CWORD]}
+  #previous word (in case it is a switch with a parameter)
+  local prev=${COMP_WORDS[COMP_CWORD-1]}
+
+  #check if the command before cursor is a switch that takes parameters, if yes,
+  #offer a choice of parameters
+  case "$prev" in
+   --cover) #for coverage we list the options explicitly
+     COMPREPLY=( $( compgen -W "assertion path branch location decision condition mcdc cover" -- $cur ) )
+     return 0
+     ;;
+   --mm) #for memory models we list the options explicitly
+     COMPREPLY=( $( compgen -W "sc tso pso" -- $cur ) )
+     return 0
+     ;;
+   --arch) #for architecture we list the options explicitly
+     COMPREPLY=( $( compgen -W "i386 x86_64" -- $cur ) )
+     return 0
+     ;;
+   -I|--classpath|-cp|--outfile|--existing-coverage|--graphml-cex)
+     #a switch that takes a file parameter of which we don't know an extension
+     #TODO probably we can do more for -I, --classpath, -cp
+     _filedir
+     return 0
+     ;;
+  esac
+
+  #complete a switch from a standard list, if the parameter under cursor starts with a hyphen
+  if [[ "$cur" == -* ]]; then
+     COMPREPLY=( $( compgen -W "$switches" -- $cur ) )
+     return 0
+  fi
+
+  #if none of the above applies, offer directories and files that we can analyze
+  _filedir "@(class|jar|cpp|cc|c\+\+|ii|cxx|c|i|gb)"
+}
+complete -F _cbmc_autocomplete cbmc

scripts/bash-autocomplete/extract_switches.sh

@@ -0,0 +1,48 @@
+#!/bin/bash
+echo "Compiling the helper file to extract the raw list of parameters from cbmc"
+g++ -c -MMD -MP -std=c++11 -Wall -I ../../src/ -ftrack-macro-expansion=0 -fno-diagnostics-show-caret switch_extractor_helper.c  -o tmp.o 2> pragma.txt
+
+retval=$?
+
+#clean up compiled files, we don't need them.
+rm tmp.o 2> /dev/null
+rm tmp.d 2> /dev/null
+
+#check if compilation went fine
+if [ $retval -ne 0 ]; then
+  echo "Problem compiling the helper file, parameter list not extracted."
+  exit 1;
+fi
+
+echo "Converting the raw parameter list to the format required by autocomplete scripts"
+rawstring=`sed "s/^.*pragma message: \(.*\)/\1/" pragma.txt`
+#delete pragma file, we won't need it
+rm pragma.txt 2> /dev/null
+
+#now the main bit, convert from raw format to a proper list of switches
+cleanstring=`(
+  #extract 2-hyphen switches, such as --foo
+  #grep for '(foo)' expressions, and then use sed to remove parantheses and put '--' at the start
+  (echo $rawstring | grep -o "([^)]*)" | sed "s/^.\(.*\).$/--\1/") ;
+  #extract 1-hyphen switches, such as -F
+  #use sed to remove all (foo) expressions, then you're left with switches and ':', so grep the colons out and then use sed to include the '-'
+  (echo $rawstring | sed "s/([^)]*)//g" | grep -o "[a-zA-Z0-9]" | sed "s/\(.*\)/-\1/")
+ ) | tr '\n' ' '`
+
+#sanity check that there is only one line of output
+if [ `echo $cleanstring | wc -l | awk '{print $1}'` -ne 1 ]; then
+ echo "Problem converting the parameter list to the correct format, I was expecting one line but either got 0 or >2. This is likely to be an error in this conversion script."
+ exit 1;
+fi
+
+#sanity check that there are no dangerous characters
+echo $cleanstring | grep -q "[^a-zA-Z0-9 -]"
+if [ $? -eq 0 ]; then
+ echo "Problem converting the parameter list to the correct format, illegal characters detected. This is likely to be an error in this conversion script."
+ exit 1;
+fi
+
+echo "Injecting the parameter list to the autocomplete file."
+sed "5 s/.*/  local switches=\"$cleanstring\"/" cbmc.sh.template > cbmc.sh
+
+rm pragma.txt 2> /dev/null

scripts/bash-autocomplete/switch_extractor_helper.c

@@ -0,0 +1,3 @@
+#include "cbmc/cbmc_parse_options.h"
+
+#pragma message CBMC_OPTIONS

src/Makefile

@@ -84,4 +84,12 @@ glucose-download:
 	@(cd ../glucose-syrup; patch -p1 < ../scripts/glucose-syrup-patch)
 	@rm glucose-syrup.tgz
 
-.PHONY: minisat2-download glucose-download
+cprover-jar-build:
+	@echo "Building org.cprover.jar"
+	@(cd java_bytecode/library/; \
+	mkdir -p target; \
+	javac -d target/ `find src/ -name "*.java"`; \
+	cd target; jar cf org.cprover.jar `find . -name "*.class"`; \
+	mv org.cprover.jar ../../../)
+
+.PHONY: minisat2-download glucose-download cprover-jar-build

src/ansi-c/ansi_c_language.cpp

@@ -196,6 +196,8 @@ Function: ansi_c_languaget::final
 
 bool ansi_c_languaget::final(symbol_tablet &symbol_table)
 {
+  generate_opaque_method_stubs(symbol_table);
+
   if(ansi_c_entry_point(symbol_table, "main", get_message_handler()))
     return true;
 

src/ansi-c/expr2c.cpp

@@ -518,28 +518,40 @@ std::string expr2ct::convert_rec(
   }
   else if(src.id()==ID_symbol)
   {
-    const typet &followed=ns.follow(src);
+    symbol_typet symbolic_type=to_symbol_type(src);
+    const irep_idt &typedef_identifer=symbolic_type.get(ID_typedef);
 
-    if(followed.id()==ID_struct)
+    // Providing we have a valid identifer, we can just use that rather than
+    // trying to find the concrete type
+    if(typedef_identifer!="")
     {
-      std::string dest=q+"struct";
-      const irep_idt &tag=to_struct_type(followed).get_tag();
-      if(tag!="")
-        dest+=" "+id2string(tag);
-      dest+=d;
-      return dest;
+      return q+id2string(typedef_identifer)+d;
     }
-    else if(followed.id()==ID_union)
+    else
     {
-      std::string dest=q+"union";
-      const irep_idt &tag=to_union_type(followed).get_tag();
-      if(tag!="")
-        dest+=" "+id2string(tag);
-      dest+=d;
-      return dest;
+      const typet &followed=ns.follow(src);
+
+      if(followed.id()==ID_struct)
+      {
+        std::string dest=q+"struct";
+        const irep_idt &tag=to_struct_type(followed).get_tag();
+        if(tag!="")
+          dest+=" "+id2string(tag);
+        dest+=d;
+        return dest;
+      }
+      else if(followed.id()==ID_union)
+      {
+        std::string dest=q+"union";
+        const irep_idt &tag=to_union_type(followed).get_tag();
+        if(tag!="")
+          dest+=" "+id2string(tag);
+        dest+=d;
+        return dest;
+      }
+      else
+        return convert_rec(followed, new_qualifiers, declarator);
     }
-    else
-      return convert_rec(followed, new_qualifiers, declarator);
   }
   else if(src.id()==ID_struct_tag)
   {