Nested axiomatic blocks

[vprevosto]

The grammar allows for nested axiomatic blocks, i.e. something like

axiomatic Foo {
  predicate foo(integer x);
  axiomatic Bar {
    predicate bar (integer x);
    axiom fb: forall integer x; foo(x) >= bar(x);
  }
}

Is it something we would really like to accept?

If yes, we should probably also be more explicit regarding inference of reads clause from axioms defining the predicates within an axiomatics (nothing is said about that in the document itself, but Jessie used to take advantage of grouping predicate/function declarations and corresponding axioms to infer the memory locations that were involved in determining the value of the predicate/function).

[vprevosto]

@pbaudin @jensgerlach @davidcok for comments

[jensgerlach]

I am not sure that nested axiomatic blocks are essential at this point.

[vprevosto]

That's a good thing, as the Frama-C implementation completely agrees with you on that point 😁