aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMelody Horn <melody@boringcactus.com>2020-10-20 10:49:44 -0600
committerMelody Horn <melody@boringcactus.com>2020-10-20 10:49:44 -0600
commit489469a7b6668bcf27362896f7a9ed4bc2a99de1 (patch)
tree5cb6e1f779801055669e849e9b3e4b63e5b2ec30
parentb7454d9c299e2b2a90d0e55157b1e7f17452f4b5 (diff)
downloadspec-489469a7b6668bcf27362896f7a9ed4bc2a99de1.tar.gz
spec-489469a7b6668bcf27362896f7a9ed4bc2a99de1.zip
add detail on C VLAs
-rw-r--r--.build.yml2
-rw-r--r--safety.md6
2 files changed, 6 insertions, 2 deletions
diff --git a/.build.yml b/.build.yml
index df36fc2..e40edc3 100644
--- a/.build.yml
+++ b/.build.yml
@@ -8,7 +8,7 @@ sources:
tasks:
- page-count: |
cd crowbar-spec
- pandoc -s -o ../spec.pdf -t html -M "TITLE=Crowbar Specification" *.md
+ pandoc -s -o ../spec.pdf -t html -M "title=Crowbar Specification" *.md
cd ..
pdfinfo spec.pdf | grep Pages
artifacts:
diff --git a/safety.md b/safety.md
index 6550492..271edc1 100644
--- a/safety.md
+++ b/safety.md
@@ -23,7 +23,11 @@ int main(int argc, (char[1024?])[argc] argv) {
}
```
-Note that `malloc` as part of the Crowbar standard library has signature `(char[size])* malloc(size_t size);` and so no cast is needed above.
+Note that `malloc` as part of the Crowbar standard library has signature `(void[size])* malloc(size_t size);` and so no cast is needed above.
+In C, `buffer` in `main` would have type pointer-to-VLA-of-char, but `buffer` in `process` would have type VLA-of-char, and this conversion would emit a compiler warning.
+However, in Crowbar, a `(T[N])*` is always implicitly convertible to `T[N]`, so no warning exists.
+(This is translated into C by dereferencing `buffer` in `main`.)
+
Note as well that the type of `argv` is complicated.
This is because the elements of `argv` have unconstrained size.
TODO figure out if that's the right way to handle that