Skip to content

Commit

Permalink
Implement lobster source filters kind and prefix (#22)
Browse files Browse the repository at this point in the history
- add integration test at integration-tests/projects/filter
- add source filter description to docs/config_files.md
  • Loading branch information
paulboege authored Feb 29, 2024
1 parent edf3af3 commit baddc9a
Show file tree
Hide file tree
Showing 16 changed files with 669 additions and 10 deletions.
1 change: 1 addition & 0 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,7 @@ packages:

integration_tests: packages
(cd integration-tests/projects/basic; make)
(cd integration-tests/projects/filter; make)

system_tests:
make -B -C test-system/lobster-json
Expand Down
10 changes: 8 additions & 2 deletions docs/config_files.md
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,14 @@ The `source` attribute assigns a LOBSTER file to contribute to this
level. There is some extra information you can supply with the `with`
keyword.

Using `with kind <string>` allows to filter items with `kind` in the
LOBSTER source file. For TRLC requirements the kind attribute in the
LOBSTER source file corresponds to the TRLC requirements type.

Using `with prefix <string>` allows to filter items with a certain
prefix in the `tag` attribute in the LOBSTER source file. For TRLC
requirements the tag attribute corresponds to the requiremet name.

Specifically for requirements you can say:

```
Expand All @@ -43,8 +51,6 @@ requirements "Requirements" {
}
```

We expect to add other `with` properties in the future.

#### trace to

The `trace to` attribute declares the expected tracing link. This
Expand Down
5 changes: 5 additions & 0 deletions integration-tests/projects/filter/.gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
cppcode.lobster
report.lobster
requirements.lobster
lobster_report.html
json.lobster
12 changes: 12 additions & 0 deletions integration-tests/projects/filter/BUILD
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
cc_library(
name = "foofunc",
srcs = ["foo.h", "foo.cpp"]
)

cc_test(
name = "foo_test",
srcs = ["test.cpp"],
deps = ["@com_google_googletest//:gtest_main",
"foofunc",
"//support/gtest/include:lobster_gtest"]
)
31 changes: 31 additions & 0 deletions integration-tests/projects/filter/Makefile
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
LOBSTER_ROOT:=../../..
LOBSTER_WIP:=$(LOBSTER_ROOT)/work-in-progress

PATH:=$(LOBSTER_ROOT)/test_install/bin:$(PATH)
PYTHONPATH:=$(wildcard $(LOBSTER_ROOT)/test_install/lib/python*/site-packages)

CLANG_TIDY:=$(LOBSTER_ROOT)/../llvm-project/build/bin/clang-tidy

THIS_TEST:=$(shell realpath --relative-to $(LOBSTER_ROOT) $(PWD))
THIS_TEST_ESCAPED:=$(subst /,\\/,$(THIS_TEST))

html_report.html: cppcode.lobster requirements.lobster lobster.conf json.lobster
@lobster-report
@lobster-online-report
@cp report.lobster report.reference_output
@lobster-html-report

cppcode.lobster: foo.h foo.cpp
@lobster-cpp foo.cpp foo.h \
--out="cppcode.lobster" --clang-tidy $(CLANG_TIDY)

requirements.lobster: example.rsl softreq_example.trlc sysreq_example.trlc
@lobster-trlc example.rsl softreq_example.trlc sysreq_example.trlc\
--out="requirements.lobster"

json.lobster: test_example.json
@lobster-json test_example.json \
--name-attribute "name" \
--tag-attribute "tags" \
--justification-attribute "justification" \
--out="json.lobster"
20 changes: 20 additions & 0 deletions integration-tests/projects/filter/example.rsl
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
package example

type System_Requirement
{
text String
}

type Software_Requirement
{
text String
trace_trlc optional System_Requirement [1 .. *]
}

checks System_Requirement {
len(text) >= 10, warning "this is a bit short", text
}

checks Software_Requirement {
len(text) >= 10, warning "this is a bit short", text
}
13 changes: 13 additions & 0 deletions integration-tests/projects/filter/foo.cpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
#include "foo.h"

int implication(int x, int y)
{
// lobster-trace: softreq_example.req_implication
return (x == 0) || (y != 0);
}

int exclusive_or(int x, int y)
{
// lobster-trace: softreq_example.req_xor
return (x == 0) != (y == 0);
}
7 changes: 7 additions & 0 deletions integration-tests/projects/filter/foo.h
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
#ifndef __FOO_H__
#define __FOO_H__

int implication(int x, int y);
int exclusive_or(int x, int y);

#endif
8 changes: 8 additions & 0 deletions integration-tests/projects/filter/lobster-trlc.conf
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
example.System_Requirement {
description = text
}

example.Software_Requirement {
description = text
tags "req" = trace_trlc
}
21 changes: 21 additions & 0 deletions integration-tests/projects/filter/lobster.conf
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
requirements "System Requirements" {
source: "requirements.lobster" with kind "System_Requirement";
}

requirements "Software Requirements"
{
source: "requirements.lobster" with kind "Software_Requirement";
trace to: "System Requirements";
}

implementation "Code"
{
source: "cppcode.lobster";
trace to: "Software Requirements";
}

activity "Verification Test"
{
source: "json.lobster";
trace to: "Software Requirements";
}
Loading

0 comments on commit baddc9a

Please sign in to comment.