Skip to content

Commit

Permalink
add and document option --fs. Release snapshot
Browse files Browse the repository at this point in the history
  • Loading branch information
pascal-cuoq committed May 16, 2016
1 parent 34493b6 commit 275f0a4
Show file tree
Hide file tree
Showing 4 changed files with 24 additions and 18 deletions.
14 changes: 7 additions & 7 deletions share/libc/__fc_machdep.h
Original file line number Diff line number Diff line change
Expand Up @@ -117,11 +117,11 @@
#define __SIZEOF_LONG 4
#define __SIZEOF_LONGLONG 8
#define __CHAR_BIT 8
#define __PTRDIFF_T long
#define __PTRDIFF_T int
#define __FC_LONG_MAX 2147483647L
#define __FC_ULONG_MAX 4294967295UL
#define __SIZE_T unsigned long
#define __FC_SIZE_MAX __FC_ULONG_MAX
#define __SIZE_T unsigned int
#define __FC_SIZE_MAX __FC_UINT_MAX

/* Optional */
#define __INTPTR_T signed long
Expand All @@ -138,11 +138,11 @@
#define __UINT_FAST32_T unsigned long

/* POSIX */
#define __SSIZE_T signed long
#define __FC_SSIZE_MAX __FC_LONG_MAX
#define __SSIZE_T signed int
#define __FC_SSIZE_MAX __FC_INT_MAX
/* stdint.h */
#define __FC_PTRDIFF_MIN __FC_LONG_MIN
#define __FC_PTRDIFF_MAX __FC_LONG_MAX
#define __FC_PTRDIFF_MIN __FC_INT_MIN
#define __FC_PTRDIFF_MAX __FC_INT_MAX

#else
#ifdef __FC_MACHDEP_PPC_32
Expand Down
9 changes: 7 additions & 2 deletions tis-interpreter/EXAMPLES.md
Original file line number Diff line number Diff line change
Expand Up @@ -62,15 +62,20 @@ be run. To run this example, we are going to need:

- `examples/03_filesystem/main.c`: the program we are interested in running
- `EXAMPLE.md`: the very file you are reading, used as input by the program
- `filesystem/__tis_mkfs.c`: the implementation for the functions `fopen` and `fread`

For the directory that contains `EXAMPLES.md`, use the commands:

```
./tis-mkfs -local EXAMPLES.md:EXAMPLES.md
./tis-interpreter.sh examples/03_filesystem/main.c filesystem/__tis_mkfs.c mkfs_filesystem.c
./tis-interpreter.sh --fs examples/03_filesystem/main.c mkfs_filesystem.c
```

The commandline option `--fs` tells tis-interpreter to link in the
filesystem implementation that provides the functions `fopen` and
`fread`. The file `mkfs_filesystem.c` has been generated by `tis-mkfs`
and contains the contents of the virtual filesystem we wish to execute
the program with.

Once the execution per se starts, you should see this file displayed
500 characters at a time. Once again, the program contains a subtle bug
(subtle enough that Valgrind probably does not catch it).
8 changes: 0 additions & 8 deletions tis-interpreter/t.c

This file was deleted.

11 changes: 10 additions & 1 deletion tis-interpreter/tis-interpreter.sh
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ TIS_PATH=$ROOT_PATH/tis-interpreter

local frama_c_binary="frama-c"

if [ -z "${TIS_INTERPRETER_USE_FRAMA_C+x}" ]
if [ -z "${TIS_INTERPRETER_USE_FRAMA_C}" ]
then
# If TIS_INTERPRETER_USE_FRAMA_C variable is not set
# then we use the local Frama-C installation.
Expand All @@ -39,6 +39,7 @@ fi

local preprocess_only="0"
local gui="0"
local filesystem="0"

local builtins="\
-val-builtin memcmp:tis_memcmp \
Expand Down Expand Up @@ -146,6 +147,9 @@ do
--gui)
gui="1";;

--fs)
filesystem="1";;

*)
others=("${others[@]}" "$1")
esac
Expand All @@ -154,6 +158,11 @@ done

local final_compiler="$compiler $compiler_opts"

if [ "Q$filesystem" = "Q1" ];
then
others=("${others[@]}" "$ROOT_PATH/filesystem/__tis_mkfs.c")
fi

if [ "Q$preprocess_only" = "Q1" ];
then
for file in "${others[@]}";
Expand Down

0 comments on commit 275f0a4

Please sign in to comment.