source: Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/cerco-executable/cerco.in @ 3215

Last change on this file since 3215 was 3215, checked in by sacerdot, 8 years ago
  • Version dumped to 0.2
  • New executable cerco to be used with why3
  • Property svn:executable set to *
File size: 1.3 KB
Line 
1#!/bin/bash
2
3MAKEFILE=@prefix@/share/frama-c-cost-plugin/makefile.cerco
4
5if [ -z "$1" -o -n "$4" -o \( -n "$2" -a -z "$3" -a \( "$1" != "-ide" -a "$1" != "-untrusted" \) \) -o \( -n "$3" -a \( \( "$1" != "-ide" -a "$1" != "-untrusted" \) -o \( "$2" != "-ide" -a "$2" != "-untrusted" \) \) \) ]; then
6        echo "Syntax: cerco [-ide] [-untrusted] filename.c"
7        exit -1
8fi
9
10if [ "$1" = "-ide" -o "$2" = "-ide" ]; then
11        SUFFIX=.why3ide
12else
13        SUFFIX=-acc.result
14fi
15
16if [ "$1" = "-untrusted" -o "$2" = "-untrusted" ]; then
17        ACC=acc
18else
19        ACC=acc-trusted
20fi
21
22if [ "$#" = 1 ]; then
23        FILENAME="$1"
24else
25        if [ "$#" = 2 ]; then
26                FILENAME="$2"
27        else
28                FILENAME="$3"
29        fi
30fi
31
32if [ ! -f $FILENAME ]; then
33        echo "Error: \"$FILENAME\" is not a regular file"
34        exit -1
35fi
36
37if [ ! -f ~/.why3.conf ]; then
38        why3config
39fi
40
41echo "Processing $FILENAME"
42
43FILENAME=`dirname $FILENAME`/`basename $FILENAME .c`
44
45function cleanup {
46        rm -rf $FILENAME-acc-instrumented.c jessie.log $FILENAME-acc-jessie.log $FILENAME-acc-annotated.jessie $FILENAME-acc.stack_cerco toto1.c $FILENAME-acc.cerco toto2.c $FILENAME-acc-framac.log $FILENAME-acc.result $FILENAME-acc.prooflog $FILENAME-acc.s
47}
48
49make -f $MAKEFILE $FILENAME$SUFFIX ACC=$ACC && cleanup
Note: See TracBrowser for help on using the repository browser.