Commit 2a92687f by Mihaela SIGHIREANU

aplas: last submission

parent c7b7f819
 ... @@ -7,7 +7,7 @@ ... @@ -7,7 +7,7 @@ \mypar{Implementation.} \mypar{Implementation.} The decision procedures presented are implemented as an extension of the The decision procedures presented are implemented as an extension of the \cspen\ solver. %~\cite{GuCW16}, \cspen\ solver, %~\cite{GuCW16}, called \cspenp, available at~\cite{CompSpenSite}. called \cspenp, available at~\cite{CompSpenSite}. %Let us briefly recall some information about {\cspen}. %Let us briefly recall some information about {\cspen}. {\cspen} is written in C++ and includes several decision procedures {\cspen} is written in C++ and includes several decision procedures ... ...
 ... @@ -15,9 +15,9 @@ conjunctions of atoms encoding ... @@ -15,9 +15,9 @@ conjunctions of atoms encoding aliasing constraints $x = y$ and $x \neq y$ between pointers $x$ and $y$, aliasing constraints $x = y$ and $x \neq y$ between pointers $x$ and $y$, points-to constraints $x\pto v$ expressing that the value $v$ is stored at the address $x$, points-to constraints $x\pto v$ expressing that the value $v$ is stored at the address $x$, and predicate atoms $P(\vec{x})$ defining (usually unbounded) memory regions of a particular structure. The points-to and predicate atoms, also called spatial atoms, and predicate atoms $P(\vec{x})$ defining (usually unbounded) memory regions of a particular structure. The points-to and predicate atoms, also called spatial atoms, are composed using the separating conjunction to specify the disjointness of memory blocks they specify. are composed using the separating conjunction to express the disjointness of memory blocks they specify. Let us briefly summarize the results on the SH fragments in the sequel. Let us briefly summarize the decidability results on the SH fragments in the sequel. For the SH fragment with the singly linked list-segment predicate, arguably the simplest SH fragment, its satisfiability and entailment problems have been shown to be in PTIME~\cite{CookHOPW11} and efficient solvers have been developed for it~\cite{SLCOMPsite}. For the SH fragment with the singly linked list-segment predicate, arguably the simplest SH fragment, its satisfiability and entailment problems have been shown to be in PTIME~\cite{CookHOPW11} and efficient solvers have been developed for it~\cite{SLCOMPsite}. % % The situation changes for more complex inductive predicates: The situation changes for more complex inductive predicates: ... ...
 ... @@ -12,7 +12,7 @@ Figure~\ref{fig:search} presents the motivating example. ... @@ -12,7 +12,7 @@ Figure~\ref{fig:search} presents the motivating example. The function \lst{search} scans The function \lst{search} scans a heap list between the addresses \lst{b} (included) a heap list between the addresses \lst{b} (included) and \lst{e} (excluded) and \lst{e} (excluded) to find a chunk of size greater than the one given as parameter. to find a chunk of size greater than the parameter \lst{rsz}. % % A heap list is a block of memory divided into \emph{chunks}, A heap list is a block of memory divided into \emph{chunks}, such that each chunk stores its size at its start address. such that each chunk stores its size at its start address. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!