added

example1/--list-options/add-source-timestamps

@@ -0,0 +1 @@
+[("x86_64-linux-ghc-7.10.1",[]),("x86_64-linux-ghc-7.8.4",[]),("x86_64-linux-ghc-7.6.3",[])]

example1/.cabal-sandbox/add-source-timestamps

@@ -0,0 +1 @@
+[("x86_64-linux-ghc-7.6.3",[])]

example1/Makefile

@@ -0,0 +1,17 @@
+default:
+	ghc main.hs
+	./main
+
+sandbox:
+	cabal exec -- ghc main.hs
+	./main
+
+val:
+	frama-c -val -main step copilot-sbv-codegen/internal.h copilot-sbv-codegen/copilot.h copilot-sbv-codegen/*.c -unspecified-access
+
+clean:
+	rm *~
+	rm main.hi
+	rm main.o
+	rm -rf copilot-c99-codegen
+	rm main

example1/cabal.sandbox.config

@@ -0,0 +1,25 @@
+-- This is a Cabal package environment file.
+-- THIS FILE IS AUTO-GENERATED. DO NOT EDIT DIRECTLY.
+-- Please create a 'cabal.config' file in the same directory
+-- if you want to change the default settings for this sandbox.
+
+
+local-repo: /home/jaloyan/Desktop/Copilot/Copilot/.cabal-sandbox/packages
+logs-dir: /home/jaloyan/Desktop/Copilot/Copilot/.cabal-sandbox/logs
+world-file: /home/jaloyan/Desktop/Copilot/Copilot/.cabal-sandbox/world
+user-install: False
+package-db: /home/jaloyan/Desktop/Copilot/Copilot/.cabal-sandbox/x86_64-linux-ghc-7.10.1-packages.conf.d
+build-summary: /home/jaloyan/Desktop/Copilot/Copilot/.cabal-sandbox/logs/build.log
+
+install-dirs
+  prefix: /home/jaloyan/Desktop/Copilot/Copilot/.cabal-sandbox
+  bindir: $prefix/bin
+  libdir: $prefix/lib
+  libsubdir: $arch-$os-$compiler/$pkgid
+  libexecdir: $prefix/libexec
+  datadir: $prefix/share
+  datasubdir: $arch-$os-$compiler/$pkgid
+  docdir: $datadir/doc/$arch-$os-$compiler/$pkgid
+  htmldir: $docdir/html
+  haddockdir: $htmldir
+  sysconfdir: $prefix/etc

example1/copilot-sbv-codegen/Makefile

@@ -0,0 +1,47 @@
+# Makefile for internal. Automatically generated by SBV. Do not edit!
+
+# include any user-defined .mk file in the current directory.
+-include *.mk
+
+CC=gcc
+CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer
+AR=ar
+ARFLAGS=cr
+
+all: internal.a
+
+internal.a: update_state_0.o update_state_1.o update_state_2.o trigger_guard_trig1.o trigger_trig1_arg_0.o trigger_trig1_arg_1.o trigger_trig1_arg_2.o ext_arr_e3.o ext_ff_1_arg0.o
+	${AR} ${ARFLAGS} $@ $^
+
+update_state_0.o: update_state_0.c internal.h
+	${CC} ${CCFLAGS} -c $< -o $@
+
+update_state_1.o: update_state_1.c internal.h
+	${CC} ${CCFLAGS} -c $< -o $@
+
+update_state_2.o: update_state_2.c internal.h
+	${CC} ${CCFLAGS} -c $< -o $@
+
+trigger_guard_trig1.o: trigger_guard_trig1.c internal.h
+	${CC} ${CCFLAGS} -c $< -o $@
+
+trigger_trig1_arg_0.o: trigger_trig1_arg_0.c internal.h
+	${CC} ${CCFLAGS} -c $< -o $@
+
+trigger_trig1_arg_1.o: trigger_trig1_arg_1.c internal.h
+	${CC} ${CCFLAGS} -c $< -o $@
+
+trigger_trig1_arg_2.o: trigger_trig1_arg_2.c internal.h
+	${CC} ${CCFLAGS} -c $< -o $@
+
+ext_arr_e3.o: ext_arr_e3.c internal.h
+	${CC} ${CCFLAGS} -c $< -o $@
+
+ext_ff_1_arg0.o: ext_ff_1_arg0.c internal.h
+	${CC} ${CCFLAGS} -c $< -o $@
+
+clean:
+	rm -f *.o
+
+veryclean: clean
+	rm -f internal.a

example1/copilot-sbv-codegen/README

@@ -0,0 +1,11 @@
+These files are automatically generated by Copilot using the SBV code generator backend.
+
+To build, you will need to ensure that all external variables and triggers are visible.
+Also, modify driver.c to include a main() function.
+Once you have a valid C program, execute
+
+  > make driver
+
+Modify the Makefile rules (Makefile and copilot.mk) as you see fit.
+
+Please report bugs to lee pike at gmail . com (remove all spaces).

example1/copilot-sbv-codegen/copilot.h

@@ -0,0 +1,28 @@
+/* Generated by Copilot Core. */
+
+#include <stdint.h>
+#include <stdbool.h>
+
+/* Observers (defined by Copilot): */
+
+
+/* Triggers (must be defined by user): */
+
+void trig1(bool, uint64_t, bool);
+
+/* External variables (must be defined by user): */
+
+extern uint64_t e1;
+extern uint64_t e2;
+
+/* External arrays (must be defined by user): */
+
+extern uint64_t e3[256];
+
+/* External functions (must be defined by user): */
+
+uint64_t ff(uint8_t);
+
+/* Step function: */
+
+void step();

example1/copilot-sbv-codegen/copilot.mk

@@ -0,0 +1,6 @@
+# Makefile rules for the Copilot driver.
+
+#CCFLAGS= -std=c99 -Werror -Wall -Wextra -Wbad-function-cast -Wcast-align -Wcast-qual -Wconversion -Wdisabled-optimization -Wformat=2 -Winit-self -Winline -Wnested-externs -Wold-style-definition -Wpointer-arith -Wredundant-decls -Wstrict-prototypes -Wswitch-default -Wswitch-enum -Wundef -Wwrite-strings -Wshadow -Wno-unused-variable -Wno-unused-but-set-variable -Wno-unused-parameter -Wno-unused-label -O2 -march=native  -c
+
+driver: driver.c copilot.h internal.a
+	${CC} ${CCFLAGS} $< -o $@ internal.a

example1/copilot-sbv-codegen/driver.c

@@ -0,0 +1,122 @@
+/* Driver for SBV program generated from Copilot. */
+/* Edit as you see fit */
+
+#include <inttypes.h>
+#include <stdbool.h>
+#include <stdint.h>
+#include <stdio.h>
+#include "internal.h"
+#include "copilot.h"
+
+/* Observers */
+
+
+/* Variables */
+SBool tmp_0 = true;
+SWord8 tmp_1 = 0;
+SBool tmp_2 = true;
+SBool queue_0[1] = { true };
+SWord8 queue_1[2] = { 0, 1 };
+SBool queue_2[2] = { true, false };
+SWord32 ptr_0 = 0;
+SWord32 ptr_1 = 0;
+SWord32 ptr_2 = 0;
+SWord64 ext_e1 = 0;
+SWord64 ext_e2 = 0;
+SWord64 ext_e3_0 = 0;
+SWord64 ext_ff_1 = 0;
+/*ACSL following*/
+/*@
+ global invariant a_bound_ptr_0: ptr_0 < 1 ; 
+ global invariant a_pos_ptr_0: ptr_0 >= 0 ; 
+ global invariant a_valid_ptr_0: \valid (queue_0 + (0.. 0 ));
+ global invariant a_bound_ptr_1: ptr_1 < 2 ; 
+ global invariant a_pos_ptr_1: ptr_1 >= 0 ; 
+ global invariant a_valid_ptr_1: \valid (queue_1 + (0.. 1 ));
+ global invariant a_bound_ptr_2: ptr_2 < 2 ; 
+ global invariant a_pos_ptr_2: ptr_2 >= 0 ; 
+ global invariant a_valid_ptr_2: \valid (queue_2 + (0.. 1 ));
+*/
+
+/*@
+ assigns ext_e1;
+ assigns ext_e2;
+ //ensures ext_e1 == e1;
+ //ensures ext_e2 == e2;
+ assigns ext_e3_0 ;
+ //ensures ext_e3_0 == tmp_e3;
+ assigns ext_ff_1;
+ //ensures ext_ff_1 == tmp_ff;
+*/
+void sampleExts(void) {
+  ext_e1 = e1;
+  ext_e2 = e2;
+  SWord64 tmp_ext_e3_0 = e3[ext_arr_e3(queue_1, ptr_1)];
+  ext_e3_0 = tmp_ext_e3_0;
+  SWord64 tmp_ff = ff(ext_ff_1_arg0(queue_1, ptr_1));
+  ext_ff_1 = tmp_ff;
+}
+
+/*@
+ assigns \nothing; 
+*/
+void fireTriggers(void) {
+  if (trigger_guard_trig1(queue_0, ptr_0))
+    trig1(trigger_trig1_arg_0(queue_1, ptr_1),
+          trigger_trig1_arg_1(ext_e1, ext_e2, ext_e3_0, ext_ff_1, queue_1, ptr_1),
+          trigger_trig1_arg_2(queue_2, ptr_2));
+}
+
+/*@
+ assigns \nothing;
+ */
+void updateObservers(void) {
+}
+
+/*@
+ assigns tmp_0;
+ assigns tmp_1;
+ assigns tmp_2;
+ */
+void updateStates(void) {
+  tmp_0 = update_state_0(queue_0, ptr_0);
+  tmp_1 = update_state_1(queue_1, ptr_1);
+  tmp_2 = update_state_2(queue_2, ptr_2, queue_1, ptr_1);
+}
+
+/*@
+ assigns queue_0[ptr_0];
+ ensures queue_0[ptr_0] == tmp_0;
+ assigns queue_1[ptr_1];
+ ensures queue_1[ptr_1] == tmp_1;
+ assigns queue_2[ptr_2];
+ ensures queue_2[ptr_2] == tmp_2;
+ */
+void updateBuffers(void) {
+  queue_0[ptr_0] = tmp_0;
+  queue_1[ptr_1] = tmp_1;
+  queue_2[ptr_2] = tmp_2;
+}
+
+/*@
+ assigns ptr_0;
+ ensures ptr_0 == (\old (ptr_0 ) + 1) % 1;
+ assigns ptr_1;
+ ensures ptr_1 == (\old (ptr_1 ) + 1) % 2;
+ assigns ptr_2;
+ ensures ptr_2 == (\old (ptr_2 ) + 1) % 2;
+ */
+void updatePtrs(void) {
+  ptr_0 = (ptr_0 + 1) % 1;
+  ptr_1 = (ptr_1 + 1) % 2;
+  ptr_2 = (ptr_2 + 1) % 2;
+}
+
+void step(void) {
+  sampleExts();
+  fireTriggers();
+  updateObservers();
+  updateStates();
+  updateBuffers();
+  updatePtrs();
+}

example1/copilot-sbv-codegen/ext_arr_e3.c

@@ -0,0 +1,31 @@
+/* File: "ext_arr_e3.c". Automatically generated by SBV. Do not edit! */
+
+#include <inttypes.h>
+#include <stdint.h>
+#include <stdbool.h>
+#include <math.h>
+#include "internal.h"
+
+/*ACSL following*/
+/*test 002*/
+/*ACSL to write
+ (s1 + 6)
+*/
+/*@
+ assigns \nothing;
+ ensures \result == (queue_1[ptr_1] + 6);
+*/
+SWord8 ext_arr_e3(const SWord8 *queue_1, const SWord32 ptr_1)
+{
+  const SWord8  s0 = queue_1[0];
+  const SWord8  s1 = queue_1[1];
+  const SWord32 s2 = ptr_1;
+  const SWord8 table0[] = {
+      s0, s1
+  };
+  const SWord32 s4 = (0x00000002UL == 0) ? s2 : (s2 % 0x00000002UL);
+  const SWord8  s5 = table0[s4];
+  const SWord8  s7 = s5 + 6;
+
+  return s7;
+}

example1/copilot-sbv-codegen/ext_ff_1_arg0.c

@@ -0,0 +1,30 @@
+/* File: "ext_ff_1_arg0.c". Automatically generated by SBV. Do not edit! */
+
+#include <inttypes.h>
+#include <stdint.h>
+#include <stdbool.h>
+#include <math.h>
+#include "internal.h"
+
+/*ACSL following*/
+/*test 003*/
+/*ACSL to write
+ s1
+*/
+/*@
+ assigns \nothing;
+ ensures \result == queue_1[ptr_1];
+*/
+SWord8 ext_ff_1_arg0(const SWord8 *queue_1, const SWord32 ptr_1)
+{
+  const SWord8  s0 = queue_1[0];
+  const SWord8  s1 = queue_1[1];
+  const SWord32 s2 = ptr_1;
+  const SWord8 table0[] = {
+      s0, s1
+  };
+  const SWord32 s4 = (0x00000002UL == 0) ? s2 : (s2 % 0x00000002UL);
+  const SWord8  s5 = table0[s4];
+
+  return s5;
+}

example1/copilot-sbv-codegen/internal.h

@@ -0,0 +1,50 @@
+/* Header file for internal. Automatically generated by SBV. Do not edit! */
+
+#ifndef __internal__HEADER_INCLUDED__
+#define __internal__HEADER_INCLUDED__
+
+#include <inttypes.h>
+#include <stdint.h>
+#include <stdbool.h>
+#include <math.h>
+
+/* The boolean type */
+typedef bool SBool;
+
+/* The float type */
+typedef float SFloat;
+
+/* The double type */
+typedef double SDouble;
+
+/* Unsigned bit-vectors */
+typedef uint8_t  SWord8 ;
+typedef uint16_t SWord16;
+typedef uint32_t SWord32;
+typedef uint64_t SWord64;
+
+/* Signed bit-vectors */
+typedef int8_t  SInt8 ;
+typedef int16_t SInt16;
+typedef int32_t SInt32;
+typedef int64_t SInt64;
+
+/* Entry point prototypes: */
+SBool update_state_0(const SBool *queue_0, const SWord32 ptr_0);
+SWord8 update_state_1(const SWord8 *queue_1, const SWord32 ptr_1);
+SBool update_state_2(const SBool *queue_2, const SWord32 ptr_2,
+                     const SWord8 *queue_1, const SWord32 ptr_1);
+SBool trigger_guard_trig1(const SBool *queue_0,
+                          const SWord32 ptr_0);
+SBool trigger_trig1_arg_0(const SWord8 *queue_1,
+                          const SWord32 ptr_1);
+SWord64 trigger_trig1_arg_1(const SWord64 ext_e1,
+                            const SWord64 ext_e2, const SWord64 ext_e3_0,
+                            const SWord64 ext_ff_1, const SWord8 *queue_1,
+                            const SWord32 ptr_1);
+SBool trigger_trig1_arg_2(const SBool *queue_2,
+                          const SWord32 ptr_2);
+SWord8 ext_arr_e3(const SWord8 *queue_1, const SWord32 ptr_1);
+SWord8 ext_ff_1_arg0(const SWord8 *queue_1, const SWord32 ptr_1);
+
+#endif /* __internal__HEADER_INCLUDED__ */