diff --git a/src/plugins/wp/MemoryContext.ml b/src/plugins/wp/MemoryContext.ml index 8d19ae6e0d173d11dbc49b60cca73e68dbb701b7..516044eb59713167d5e34722e58a0628cd5ca851 100644 --- a/src/plugins/wp/MemoryContext.ml +++ b/src/plugins/wp/MemoryContext.ml @@ -46,7 +46,7 @@ type zone = | Var of varinfo (* &x - the cell x *) | Ptr of varinfo (* p - the cell pointed by p *) | Arr of varinfo (* p+(..) - the cell and its neighbors pointed by p *) - | Term of term + | Term of term (* use the ACSL term as is *) type partition = { globals : zone list ; (* [ &G , G[...], ... ] *)