From d63b2c0cca14bc5b0f432dacbdbe556021184fd2 Mon Sep 17 00:00:00 2001
From: Ben Karel <eschew@gmail.com>
Date: Fri, 2 May 2025 16:07:48 -0400
Subject: [PATCH] Update README for dune-built CodeHawk

---
 README.md                     | 41 +++++++++++++++--------------------
 chc/util/ConfigLocal.template |  2 --
 2 files changed, 18 insertions(+), 25 deletions(-)

diff --git a/README.md b/README.md
index b15cbb1..9bf8222 100644
--- a/README.md
+++ b/README.md
@@ -4,33 +4,28 @@ Sound Static Analysis of C for Memory Safety (Undefined Behavior)
 ### Quick start
 
 The CodeHawk-C Analyzer consists of two parts:
-- A python front end (this repository) through which all user interaction
+- A Python front end (this repository) through which all user interaction
   is performed, and
-- An ocaml abstract-interpretation engine that powers the analysis.
+- An OCaml abstract-interpretation engine that powers the analysis.
 
-To use the CodeHawk-C Analyzer first clone or download the ocaml application
+To use the CodeHawk-C Analyzer first clone or download the OCaml application
 from
 ```
 https://github.com/static-analysis-engineering/codehawk
 ```
-and build according to the accompanying instructions given there.
-Then copy the following files from that build:
-```
-codehawk/CodeHawk/CHC/cchcil/parseFile
-codehawk/CodeHawk/CHC/cchcmdline/canalyzer
-```
-to the following location in this repository:
-```
-CodeHawk-C/chc/bin/linux/
-```
-or
-```
-CodeHawk-C/chc/bin/macOS
-```
-depending on the platform where the executables were built.
-Alternatively, you can edit the path to these two executables directly
-in chc/util/Config.py or chc/util/ConfigLocal.py, so there is no need
-to copy them or update them with each new version of the ocaml analyzer.
+and build with `dune` according to the accompanying instructions given there.
+
+You can either:
+- Copy `chc/util/ConfigLocal.template` to `chc/util/ConfigLocal.py`
+in this repository, and edit the latter file to set the paths for
+`config.canalyzer` and `config.cparser` to the `dune`-built binaries,
+which should be in `your-path-to-codehawk/CodeHawk/_build/install/default/bin/`.
+This allows CodeHawk-C to automatically use newly-built versions of the
+OCaml analyzer.
+- Or, you can copy the `canalyzer` and `parseFile` binaries from that location
+into `chc/bin/linux/` or `chc/bin/macOS` within this repository.
+To allow CodeHawk-C to use newly-built versions of the OCaml analyzer,
+you will have to re-copy the binaries after every build.
 
 Set the python path and path:
 ```
@@ -47,8 +42,8 @@ which should show something like:
 Analyzer configuration:
 -----------------------
   platform : linux
-  parser   : /home/user/codehawk/CodeHawk/CHC/cchcil/parseFile (found)
-  analyzer : /home/user/codehawk/CodeHawk/CHC/cchcmdline/canalyzer (found)
+  parser   : /home/user/codehawk/CodeHawk/_build/install/default/bin/parseFile (found)
+  analyzer : /home/user/codehawk/CodeHawk/_build/install/default/bin/canalyzer (found)
 
   summaries: /home/user/CodeHawk-C/chc/summaries/cchsummaries.jar (found)
 ```
diff --git a/chc/util/ConfigLocal.template b/chc/util/ConfigLocal.template
index 8b69c54..e1237c4 100644
--- a/chc/util/ConfigLocal.template
+++ b/chc/util/ConfigLocal.template
@@ -46,6 +46,4 @@ def getLocals(config: chc.util.Config.Config) -> None:
     config.canalyzer = '/home/username/my-analyzer/canalyzer'
     config.cparser = '/home/username/my-parser/parseFile'
     config.summaries = '/home/username/my-summaries/cchsummaries.jar'
-    config.bear = '/home/username/bear-home/bear'
-    config.libear = '/home/username/bear-home/libear.so'
     '''