Merge pull request #447 from kind2-mc/develop

Docker and travis tweaks, interpreter fixes

.travis-ci.sh

@@ -31,17 +31,5 @@ eval $(opam config env)
 ./autogen.sh
 ./build.sh
 
-# Checking regression test first.
+# Checking regression test .
 make test
-
-# Retrieve and build Kind 2 develop.
-dev_dir="kind2-dev"
-git clone https://github.com/kind2-mc/kind2 $dev_dir
-cd $dev_dir
-./autogen.sh
-./build.sh
-cd ..
-cp $dev_dir/bin/kind2 bin/kind2-dev
-
-# Unimplemented.
-ls bin/

.travis.yml

@@ -1,3 +1,7 @@
+branches:
+  only:
+  - develop
+  - master
 language: c
 sudo: required
 script: bash -ex .travis-ci.sh

Dockerfile

@@ -54,12 +54,7 @@ RUN chmod a+x bin/cvc4
 RUN mkdir kind2
 COPY . kind2/
 WORKDIR kind2
-RUN if [ -f "Makefile" ] ; then make clean ; fi
-RUN rm -rf src/_build configure Makefile
-RUN rm -rf bin
-RUN rm -rf src/Makefile src/kind2.native
-# RUN ls src
-RUN autoreconf
+RUN if [ -f "Makefile" ] ; then make clean && rm -rf src/_build configure Makefile && rm -rf bin && rm -rf src/Makefile src/kind2.native && autoreconf ; fi
 RUN ./autogen.sh
 RUN ./build.sh
 WORKDIR ./..

README.md

@@ -1,5 +1,8 @@
 # Kind 2
 
+`develop`: [![Build Status](https://travis-ci.org/kind2-mc/kind2.svg?branch=develop)](https://travis-ci.org/kind2-mc/kind2)
+`master`: [![Build Status](https://travis-ci.org/kind2-mc/kind2.svg?branch=master)](https://travis-ci.org/kind2-mc/kind2)
+
 A multi-engine, parallel, SMT-based automatic model checker for safety properties of Lustre programs.
 
 Kind 2 takes as input a Lustre file annotated with properties to be proven

src/interpreter.ml

@@ -82,6 +82,26 @@ let main input_file input_sys aparam trans_sys =
 
   let nb_inputs = List.filter StateVar.is_input trans_svars |> List.length in
 
+  (* Check that constant inputs are indeed constant. *)
+  inputs |> List.iter (
+    function
+    | (sv, head :: tail) when StateVar.is_const sv ->
+      tail |> List.fold_left (
+        fun acc value ->
+          if acc != value then (
+            Event.log L_warn
+              "Input %s is constant, but input values differ: \
+              got %a and, later, %a."
+              (StateVar.name_of_state_var sv)
+              Term.pp_print_term acc
+              Term.pp_print_term value ;
+            Failure "main" |> raise
+          ) ;
+          acc
+      ) head |> ignore
+    | _ -> ()
+  ) ;
+
   (* Remove sliced inputs *)
   let inputs = List.filter (fun (sv, _) ->
       List.exists (StateVar.equal_state_vars sv) trans_svars
@@ -106,8 +126,8 @@ let main input_file input_sys aparam trans_sys =
 
          (* Output warning *)
          Event.log L_warn 
-           "Input for %a is longer than other inputs"
-           StateVar.pp_print_state_var state_var)
+           "Input for %s is longer than other inputs"
+           (StateVar.name_of_state_var state_var))
 
     inputs;
 

src/kind2Flow.ml

@@ -477,7 +477,7 @@ let run in_sys =
     | Some param ->
       (* Build trans sys and slicing info. *)
       let sys, in_sys_sliced =
-        ISys.trans_sys_of_analysis in_sys param
+        ISys.trans_sys_of_analysis ~preserve_sig:true in_sys param
       in
       (* Set module currently running. *)
       Event.set_module m ;