Skip to content

Commit

Permalink
Fix titles
Browse files Browse the repository at this point in the history
  • Loading branch information
francescoo22 committed Sep 12, 2024
1 parent 0ac7695 commit 574b6b0
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 3 deletions.
2 changes: 1 addition & 1 deletion chapters/1-Introduction.typ
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ The thesis finally shows how aligning Kotlin’s memory model with Viper’s, us
intro-kt-annotated
)<kt-ann-intro>

== Structure of the thesis
== Structure of the Thesis

The rest of the thesis is organized as follows:

Expand Down
4 changes: 2 additions & 2 deletions chapters/6-Encoding.typ
Original file line number Diff line number Diff line change
Expand Up @@ -105,13 +105,13 @@ When no predicates contain the access to a property that needs to be accessed, i

Encoding method calls is straightforward for some cases, but requires attention for some others.

=== Functions with unique parameters
=== Functions with Unique Parameters

Functions with a unique parameter, when called, do not need the inclusion of additional statements for their encoding, except for folding or unfolding statements, as detailed in @cap:unfolding.

#code-compare("Function call with unique parameter encoding", .8fr, unique-call-kt, unique-call-vpr)

=== Functions with shared parameters
=== Functions with Shared Parameters

When functions with a shared parameter are called, their encoding may require the addition of `inhale` and `exhale` statements. The annotation system allows functions with shared parameters to be called by passing unique references. However, the function's conditions alone are not sufficient to properly encode these calls.

Expand Down

0 comments on commit 574b6b0

Please sign in to comment.