summaryrefslogtreecommitdiff
path: root/examples/program_analysis/paper_demos/bash.txt
diff options
context:
space:
mode:
authorMatthew Sotoudeh <matthewsot@outlook.com>2020-11-10 14:06:35 -0800
committerMatthew Sotoudeh <matthewsot@outlook.com>2020-11-10 14:06:35 -0800
commit904094281b062aff3445ca41fec57e4cfd0f563d (patch)
treeed49271ab1ff8448a433921533159f6a8e450c8b /examples/program_analysis/paper_demos/bash.txt
parentdb99b3af36fa4687c734e1c74d83157d2f10c9ed (diff)
Initial code release
Diffstat (limited to 'examples/program_analysis/paper_demos/bash.txt')
-rw-r--r--examples/program_analysis/paper_demos/bash.txt17
1 files changed, 17 insertions, 0 deletions
diff --git a/examples/program_analysis/paper_demos/bash.txt b/examples/program_analysis/paper_demos/bash.txt
new file mode 100644
index 0000000..083401c
--- /dev/null
+++ b/examples/program_analysis/paper_demos/bash.txt
@@ -0,0 +1,17 @@
+int cd_builtin (list) WORD_LIST *list; /*@\color{red}{//B1} @*/
+{
+ char *dirname, *cdpath, *path, *temp;
+...
+
+struct builtin static_shell_builtins[] = {
+...
+ { "cd", cd_builtin, ... }, /*@\color{red}{//B2} @*/
+...
+struct builtin *shell_builtins = static_shell_builtins; /*@\color{red}{//B3} @*/
+
+struct builtin * builtin_address_internal
+ (name, disabled_okay)
+ char *name; int disabled_okay; { /*@\color{red}{//B4} @*/
+...
+ j = shell_builtins[mid].name[0] - name[0];
+...
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback