blob: 85e8ba48dea092aa6e95ba7a70f1005b520caaaf (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
+++
title = "Base pointer of main memory"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3c6"]
forwardlinks = ["3c6b"]
zettelid = "3c6a"
+++
One of the current limitations of function calls in HTL is that they
don't support any loads or stores in these functions. This is because
Vericert currently only generates one global memory. Therefore, there
should not be any pointers in the program that have a base pointer that
is different to the base pointer of the main function's stack.
One possible solution to this is to find what the base of the stack is,
and then prove if we ever have a base pointer.
|
