diff --git a/README.md b/README.md
index e589d64d1ffcbec6daa5e8bf4f24d1dc79655f39..b366e8309d40e66b9d6d67d7b41f10ea58bf4a2c 100644
--- a/README.md
+++ b/README.md
@@ -2,15 +2,16 @@
WSymb: Symbolic Worst-Case Execution Time (WCET) computation.
-* Version 1.0.0 (for OTAWA v2), April 2020
+* Version 1.1 (for OTAWA v2), December 2023
----
## Authors
* Clement Ballabriga <Clement.Ballabriga@nospamuniv-lille.fr>
* Julien Forget <Julien.Forget@nospamuniv-lille.fr>
-* Celestine Sauvage <celestine.sauvage@nospamgmail.com>
* Sandro Grebant <sandro.grebant@nospamuniv-lille.fr>
+* Giuseppe Lipari <giuseppe.lipari@nospamuniv-lille.fr>
+* Celestine Sauvage <celestine.sauvage@nospamgmail.com>
License: GPL 2.1 or higher.
@@ -20,12 +21,12 @@ Please remove "nospam" from the email addresses.
## Introduction
-WSymb is a WCET analysis tool. Its main specificity is that, instead of
-a constant WCET, it computes a *WCET formula*, where symbols (or
-parameters) can correspond to various kinds of values unnkown at analysis
-time. The formula can later be *instanciated*, when parameter values are
-known. For more details on the underlying theory, check out the papers
-[1,2].
+WSymb is a WCET analysis tool. Its main specificity is that, instead
+of a constant WCET, it computes a *WCET formula*, where symbols (or
+parameters) can correspond to various kinds of values unnkown at
+analysis time. The formula can later be *instanciated*, when parameter
+values are known. For more details on the underlying theory, check out
+the papers [1,2].
WSymb consists of several separate parts:
@@ -43,6 +44,12 @@ WSymb consists of several separate parts:
* The instantiation of the WCET formula relies on an API documented in
`pwcet/include/pwcet-tuntime.h`.
+* `WCET-procedure-arguments-as-parameters.md`: this file describes an
+ extension to the original analysis, which analyzes the binary code
+ of a procedure to produce a WCET formula that represents the WCET of
+ the procedure as a function of its arguments. It implements the
+ approach presented in [2].
+
A complete example covering all these different parts is provided in
directory `example`.
@@ -163,8 +170,11 @@ so:
----
## References
-[1] Ballabriga, C., Forget, J., & Lipari, G. (2018). Symbolic WCET computation. ACM Transactions on Embedded Computing Systems (TECS), 17(2), 39.
-ISO 690
-
-[2] https://arxiv.org/abs/1709.09369
+[1] Ballabriga, C., Forget, J., Lipari, G. (2018). Symbolic WCET
+computation. ACM Transactions on Embedded Computing Systems (TECS),
+17(2), 39. https://hal.science/hal-01665076
+[2] Grebant S, Ballabriga C, Forget J, Lipari G. WCET analysis with
+procedure arguments as parameters. InProceedings of the 31st
+International Conference on Real-Time Networks and Systems 2023 Jun 7
+(pp. 11-22). https://hal.science/hal-04118213
diff --git a/WCET-procedure-arguments-as-parameters.md b/WCET-procedure-arguments-as-parameters.md
index 93a3c684be46c5a0621e4a78e616c5355beec9a0..43d2d706763b5880134594e6ad3a9c5d9d81599e 100644
--- a/WCET-procedure-arguments-as-parameters.md
+++ b/WCET-procedure-arguments-as-parameters.md
@@ -1,7 +1,5 @@
# WCET analysis with procedure arguments as parameters
-* Version 1.0.0, November 2023
-
----
## Authors
@@ -27,12 +25,10 @@ arguments. It implements the approach presented in [1].
Required packages:
- WSymb, cloned from its
- [git](https://gitlab.cristal.univ-lille.fr/otawa-plugins/polymalys)
- branch ``input conditionals``;
+ [git](https://gitlab.cristal.univ-lille.fr/otawa-plugins/polymalys);
- Otawa for WSymb (see instructions in the README.md of WSymb);
- Polymalys, cloned from its
- [git](https://gitlab.cristal.univ-lille.fr/otawa-plugins/WSymb),
- branch ``input conditionals``;
+ [git](https://gitlab.cristal.univ-lille.fr/otawa-plugins/WSymb);
- Otawa for Polymalys (see instructions in the README.md of Polymalys);
- Basic compilation tools (make, gcc, g++, as well as the arm
versions).
@@ -71,12 +67,10 @@ In the following, the required version is specified when necessary.
### Polymalys
-
-
Compile Polymalys (using Otawa for Polymalys):
```shell
-./do_in.sh polymalys cd <polymalys>; make install cd tests; make poly
+./do_in.sh polymalys make -C <polymalys> install; make -C <polymalys>/tests poly
```
### WSymb
@@ -84,7 +78,7 @@ Compile Polymalys (using Otawa for Polymalys):
Compile and install WSymb (using Otawa for WSymb):
```shell
-./do_in.sh wsymb cd <wsymb>; make install; cd simplify; make; cd libpwcet; make
+./do_in.sh wsymb make -C <wsymb> install; make -C <wsymb>/simplify; make -C <wsymb>/libpwcet
```
----
@@ -106,7 +100,7 @@ file wih Otawa (any of the two Otawa versions should produce the same
result):
```shell
-./do_in.sh wsymb <otawa-wsymb>/bin/mkff <programme>.elf [function] > programme.elf
+./do_in.sh wsymb <otawa-wsymb>/bin/mkff <programme>.elf [function] > <programme>.ff
```
Specifying the function is optional. If the function is not specified,
diff --git a/do_in.sh b/do_in.sh
index 287ebf64392d96d40de12d27f319b82233067325..c5979795ab4f31048a33facca45aaaf49a6fd9e9 100755
--- a/do_in.sh
+++ b/do_in.sh
@@ -1,18 +1,16 @@
#!/bin/sh
-# update the two first variables as necessary
+# update the two variables below as necessary
-OTAWA_POLY=/home/forget/Code/WSymb-procedures/polymalys/otawa
-OTAWA_WSYMB=/home/forget/Code/WSymb-procedures/otawa
+OTAWA_POLY=/home/forget/Code/polymalys/otawa
+OTAWA_WSYMB=/home/forget/Installs/otawa-wsymb/otawa
case $1 in
"polymalys" )
- echo "Executing with Otawa version Polymalys"
export PATH=$OTAWA_POLY/bin/:$PATH
export LD_LIBRARY_PATH=$OTAWA_POLY/lib/:$OTAWA_POLY/lib/otawa/otawa/:$LD_LIBRARY_PATH
shift
$*;;
"wsymb" )
- echo "Executing Otawa version WSymb"
export PATH=$OTAWA_WSYMB/bin:$PATH
export LD_LIBRARY_PATH=$OTAWA_WSYMB/lib:$OTAWA_WSYMB/lib/otawa/otawa:$LD_LIBRARY_PATH
shift