Add support for throws clauses in ACSL function contracts

[hugo-saci]

Add support for throws clauses in ACSL function contracts.

This is based on the grammar of a throws-clause from ACSL++ (figure 2.28):
throws pred ;
throws { C-type-name (, C-type-name )* } pred ;

The ACSL-parser has been extended to support the syntax above in function contracts.

The FunctionContract is encoded differently in ACSLTransator.scala, accounting for throws clauses. This encoding is based on the global exception variables that are generated in CCAstExceptionTransformer.scala.

Information from the TriCera preprocessor (tri-pp) is used to determine if the throws clauses should be accounted for. If the program does not contain exceptions, throws clauses are ignored (a warning is given if throws clauses exist) and the FunctionContract is encoded as previously done.

Not supported

In ACSL++, and \exception term is defined to be a pointer to the exception object. This has NOT been implemented.

Mathematical description

For programs that contain exceptions, here is how the contract is encoded. Given non-exceptional precondition $P$, locations $L$, and postcondition $Q$, the exceptional contract is defined by $\hat{P}, \hat{L}, \hat{Q}$.

Given throws clauses:
throws $P_1$;
$\vdots$
throws $P_m$;
throws { $T^1_1, \dots, T^1_{t_1}$ } $P_1'$;
$\vdots$
throws { $T^k_1, \dots, T^k_{t_k}$ } $P'_k$;

and the following:

• $\hat{e}$ is the exception flag variable (__exception_flag)
• $\hat{e_T}$ is the exception type variable (__exception_type)
• $\hat{e_v}$ is the exception value variable (__exception_value)
• $\mathbf{T}_e$ is the set of exception types in the program

Here is how the exceptional contract is defined:

$$ \hat{P} \ \overset{\mathrm{def}}{=} \ P \wedge \hat{e} = 0 $$

$$ \hat{L} \ \overset{\mathrm{def}}{=} \ L \cup \{ \hat{e}, \hat{e_T}, \hat{e_v} \}. $$

$$ \hat{Q} \ \overset{\mathrm{def}}{=} \ (\hat{e} = 0 \to Q) \wedge (\hat{e} \neq 0 \to E) $$

where

$$ E \ = \ \underbrace{\hat{e_T} \in \mathbf{T}_e}_{\text{valid type}} \ \ \ \ \ \wedge \underbrace{\bigwedge_{1 \leq i \leq m} P_i}_{\text{clauses without types}} \wedge \ \ \ \ \underbrace{\bigwedge_{1 \leq i \leq k} \left( \hat{e_T} \in \{ T^i_1, \dots, T^i_{t_i} \} \to P'_i \right)}_{\text{clauses with types}}. $$

• To the precondition, it is added that the exception flag must not be set when a function is entered.
• The global exception variables are added to the set of assignable locations.
• For the postcondition: If normal termination, then the "normal" postcondition should hold, if exceptional termination, then
  1. the exception type must be one of the exception types in the program
  2. the predicates in the clauses without types must all hold
  3. for the predicates in clauses with types: if the exception type is one of the types, then the predicate must hold