Commit a3c6acc4 authored by Sergio Costas's avatar Sergio Costas

Updated the documentation

parent bbeed7f4
......@@ -120,7 +120,16 @@ This can be done with the **-e** statement:
will process all files whose name end with *.c* except *sourcefile.c*.
## MEMORY MODEL
## MANAGEMENT MODEL
Before reading this, it is strongly recommended to read the chapter
"understanding ownership" from the RUST tutorial, because the model
used in CRUST is mainly the same.
https://doc.rust-lang.org/beta/book/second-edition/ch04-00-understanding-ownership.html
Also it can be useful to check the **unitest** folder, with all the
tests and the comments that explain why something is right or wrong.
CRUST presumes that every CRUST-type pointer can be in one of the
following states:
......@@ -136,7 +145,8 @@ following states:
is a dangling pointer.
It also mandates that each memory block must be pointed by one, and
only one, CRUST variable (there is an exception with aliases).
only one, CRUST variable (there is an exception with aliases, and
global variables).
CRUST follows all the possible execution branches for each of the
functions in the source file. When it starts with a function, each of
......@@ -151,14 +161,16 @@ in a memory leak.
If a function returns a CRUST value, it is also an error to not store it
in a CRUST variable, because it also results in a memory leak. The only
exception is when the return value is marked as *borrowed*.
exception is when the return value is marked as *borrowed*, in which case
it must be stored in a CRUST *borrowed* variable.
Every time a CRUST variable is passed as an argument to a function, the
ownership is passed too, so, from that point, it will be in the FREED
state because it is assumed that the block has been freed in the called
function. There is an exception, and it is when the argument in the called
function is marked as *borrowed*. In that case, the called function can't
free the block, but can modify it.
state inside the calling function because it is assumed that the block
has been freed in the called function. There is an exception, and it is
when the argument in the called function is marked as *borrowed*. In that
case, the called function can't free the block, but can modify it, because
the ownership is retained in the caller function.
Trying to use a CRUST variable that is in UNINITIALIZED or FREED status is
an error, either using it as an argument when calling a function or accessing
......@@ -166,6 +178,13 @@ them through indirection (in the case of a pointer to a struct), because,
in the case of FREED status, that block has already been freed (it is a
dangling pointer).
Global variables are an special case: since it is not possible to know
its state (because it can be changed outside the current function), they
are assumed to be in NOT_NULL_OR_NULL status when used as the origin, and
in UNINITIALIZED status when used as the destination. But it is important
to remember that assigning a CRUST variable to a global CRUST variable will
mark the former as FREED.
CRUST understand some comparisons, so this code:
if (crust_variable == NULL) {
......@@ -173,7 +192,7 @@ CRUST understand some comparisons, so this code:
}
will never produce an error, because if *crust_variable* has a NOT_NULL_OR_NULL
status, the code evaluation will branch in two at the **if** statement, one
status before the IF statement, the code evaluation will branch in two, one
where it has the NULL status (that will evaluate the call to the function), and
another with a NOT_NULL status, that will evaluate only the code after the **if**
statement.
......@@ -183,14 +202,6 @@ CRUST-type variables are checked, and it is an error that they are in NOT_NULL o
NOT_NULL_OR_NULL status (unless they are *borrowed*). Doing so would lead again
to memory leaks.
For more details, it is strongly recommended to read the chapter "understanding
ownership" from the RUST tutorial, because the model used in CRUST is mainly
the same.
https://doc.rust-lang.org/beta/book/second-edition/ch04-00-understanding-ownership.html
Also it can be useful to check the **unitest** folder, with all the tests and the
comments that explain why something is right or wrong.
# CURRENT STATUS
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment