From ddd56a68e62a480ee188256e7e33c72e65407514 Mon Sep 17 00:00:00 2001 From: Andre Maroneze <andre.maroneze@cea.fr> Date: Fri, 2 Sep 2022 10:37:00 +0200 Subject: [PATCH] [Doc] remove obsolete files --- doc/developer/hello_world/Makefile | 32 ---- doc/developer/hello_world/hello_world.ml | 67 ------- doc/developer/tutorial/hello/Makefile | 223 ----------------------- 3 files changed, 322 deletions(-) delete mode 100644 doc/developer/hello_world/Makefile delete mode 100644 doc/developer/hello_world/hello_world.ml delete mode 100644 doc/developer/tutorial/hello/Makefile diff --git a/doc/developer/hello_world/Makefile b/doc/developer/hello_world/Makefile deleted file mode 100644 index 8da55444dd6..00000000000 --- a/doc/developer/hello_world/Makefile +++ /dev/null @@ -1,32 +0,0 @@ -########################################################################## -# # -# This file is part of Frama-C. # -# # -# Copyright (C) 2007-2022 # -# CEA (Commissariat à l'énergie atomique et aux énergies # -# alternatives) # -# # -# you can redistribute it and/or modify it under the terms of the GNU # -# Lesser General Public License as published by the Free Software # -# Foundation, version 2.1. # -# # -# It is distributed in the hope that it will be useful, # -# but WITHOUT ANY WARRANTY; without even the implied warranty of # -# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # -# GNU Lesser General Public License for more details. # -# # -# See the GNU Lesser General Public License version 2.1 # -# for more details (enclosed in the file licenses/LGPLv2.1). # -# # -########################################################################## - -# Example of Makefile for dynamic plugins -######################################### - -# Frama-c should be properly installed with "make install" -# before any use of this makefile - -FRAMAC_SHARE :=$(shell frama-c-config -print-share-path) -PLUGIN_NAME = Hello -PLUGIN_CMO = hello_world -include $(FRAMAC_SHARE)/Makefile.dynamic diff --git a/doc/developer/hello_world/hello_world.ml b/doc/developer/hello_world/hello_world.ml deleted file mode 100644 index 42a651ff49a..00000000000 --- a/doc/developer/hello_world/hello_world.ml +++ /dev/null @@ -1,67 +0,0 @@ -(**************************************************************************) -(* *) -(* This file is part of Frama-C. *) -(* *) -(* Copyright (C) 2007-2022 *) -(* CEA (Commissariat à l'énergie atomique et aux énergies *) -(* alternatives) *) -(* *) -(* you can redistribute it and/or modify it under the terms of the GNU *) -(* Lesser General Public License as published by the Free Software *) -(* Foundation, version 2.1. *) -(* *) -(* It is distributed in the hope that it will be useful, *) -(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) -(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) -(* GNU Lesser General Public License for more details. *) -(* *) -(* See the GNU Lesser General Public License version 2.1 *) -(* for more details (enclosed in the file licenses/LGPLv2.1). *) -(* *) -(**************************************************************************) - -(** The traditional 'Hello world!' plugin. - It contains one boolean state [Enabled] which can be set by the - command line option "-hello". - When this option is set it just pretty prints a message on the standard - output. *) - -(** Register the new plug-in "Hello World" and provide access to some plug-in - dedicated features. *) -module Self = - Plugin.Register - (struct - let name = "Hello world" - let shortname = "hello" - let help = "The famous 'Hello world' plugin" - end) - -(** Register the new Frama-C option "-hello". *) -module Enabled = - Self.False - (struct - let option_name = "-hello" - let help = "pretty print \"Hello world!\"" - end) - -let print () = Self.result "Hello world!" - -(** The function [print] below is not mandatory: you can ignore it in a first - reading. It provides an API for the plug-in, so that the function [run] is - callable by another plug-in: each plug-in can call - [Dynamic.get "Hello.run" (Datatype.func Datatype.unit Datatype.unit)] in - order to call [print]. *) -let print = - Dynamic.register - ~comment:"[Dynamic.get \"Hello.run\" (Datatype.func Datatype.unit \ - Datatype.unit)] calls [run] and pretty prints \"Hello world!\"" - ~plugin:"Hello" - "run" - (Datatype.func Datatype.unit Datatype.unit) - print - -(** Print 'Hello World!' whenever the option is set. *) -let run () = if Enabled.get () then print () - -(** Register the function [run] as a main entry point. *) -let () = Db.Main.extend run diff --git a/doc/developer/tutorial/hello/Makefile b/doc/developer/tutorial/hello/Makefile deleted file mode 100644 index e3d5af7cece..00000000000 --- a/doc/developer/tutorial/hello/Makefile +++ /dev/null @@ -1,223 +0,0 @@ -########################################################################## -# # -# This file is part of Frama-C. # -# # -# Copyright (C) 2007-2022 # -# CEA (Commissariat à l'énergie atomique et aux énergies # -# alternatives) # -# # -# you can redistribute it and/or modify it under the terms of the GNU # -# Lesser General Public License as published by the Free Software # -# Foundation, version 2.1. # -# # -# It is distributed in the hope that it will be useful, # -# but WITHOUT ANY WARRANTY; without even the implied warranty of # -# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # -# GNU Lesser General Public License for more details. # -# # -# See the GNU Lesser General Public License version 2.1 # -# for more details (enclosed in the file licenses/LGPLv2.1). # -# # -########################################################################## - -PLUGIN_DIRS = empty simple with_registration with_log multiple with_options with_test with_doc -FINAL_PLUGINS = $(patsubst %,generated/%,$(PLUGIN_DIRS)) -DIRS = generated $(addprefix generated/, src $(PLUGIN_DIRS)) - -all: clean $(FINAL_PLUGINS) - -generated/src/dune: src/dune - mkdir -p $(dir $@) - cp $< $@ - headache -c ../../../../headers/headache_config.txt -r $@ - -generated/src/dune-project: src/dune-project - mkdir -p $(dir $@) - cp $< $@ - headache -c ../../../../headers/headache_config.txt -r $@ - -generated/src/%.ml: src/%.ml - mkdir -p $(dir $@) - cp $< $@ - headache -r $@ - -generated/src/tests/ptests_config: src/ptests_config - mkdir -p $(dir $@) - cp $< $@ - -generated/src/tests/test_config: src/test_config - mkdir -p $(dir $@) - cp $< $@ - -generated/src/tests/hello/%.c: src/%.c - mkdir -p $(dir $@) - cp $< $@ - headache -r $@ - -generated/src/tests/hello/oracle/%.oracle: src/%.oracle - mkdir -p $(dir $@) - cp $< $@ - -generated/%/Hello.ml: src/Hello.ml - mkdir -p $(dir $@) - cp $< $@ - headache -r $@ - -generated/empty: generated/src/dune \ - generated/src/dune-project \ - generated/src/Hello.ml - mkdir -p $@ - cp generated/src/dune $@/dune - cp generated/src/dune-project $@/dune-project - cp generated/src/Hello.ml $@/Hello.ml - -generated/simple: generated/empty \ - generated/src/run_print_to_file.ml \ - generated/src/extend_run.ml - mkdir -p $@ - cp generated/empty/* $@ - for i in $(filter %.ml, $^); do \ - cat $$i >> $@/hello_world.ml; \ - echo "" >> $@/hello_world.ml; \ - done - -generated/with_registration: generated/empty \ - generated/src/help_msg.ml \ - generated/src/register.ml \ - generated/src/run_print_to_file.ml \ - generated/src/extend_run.ml - mkdir -p $@ - cp generated/empty/* $@ - for i in $(filter %.ml, $^); do \ - cat $$i >> $@/hello_world.ml; \ - echo "" >> $@/hello_world.ml; \ - done - -generated/with_log: generated/empty \ - generated/src/help_msg.ml \ - generated/src/register.ml \ - generated/src/run_log.ml \ - generated/src/extend_run.ml - mkdir -p $@ - cp generated/empty/* $@ - for i in $(filter %.ml, $^); do \ - cat $$i >> $@/hello_world.ml; \ - echo "" >> $@/hello_world.ml; \ - done - -generated/with_options: generated/empty \ - generated/src/help_msg.ml \ - generated/src/register.ml \ - generated/src/options_enabled.ml \ - generated/src/options_output_file.ml \ - generated/src/run_with_options.ml \ - generated/src/extend_run.ml - mkdir -p $@ - cp generated/empty/* $@ - for i in $(filter %.ml, $^); do \ - cat $$i >> $@/hello_world.ml; \ - echo "" >> $@/hello_world.ml; \ - done - -generated/multiple: generated/empty \ - generated/src/help_msg.ml \ - generated/src/register.ml \ - generated/src/options_enabled.ml \ - generated/src/options_output_file.ml \ - generated/src/print.ml \ - generated/src/run_call_print.ml \ - generated/src/extend_run.ml - mkdir -p $@ - cp generated/empty/* $@ - cp generated/src/help_msg.ml $@/hello_options.ml - echo "" >> $@/hello_options.ml - cat generated/src/register.ml >> $@/hello_options.ml - echo "" >> $@/hello_options.ml - cat generated/src/options_enabled.ml >> $@/hello_options.ml - echo "" >> $@/hello_options.ml - cat generated/src/options_output_file.ml >> $@/hello_options.ml - cp generated/src/print.ml $@/hello_print.ml - cp generated/src/run_call_print.ml $@/hello_run.ml - echo "" >> $@/hello_run.ml - cat generated/src/extend_run.ml >> $@/hello_run.ml - -generated/with_test: generated/multiple \ - generated/src/run_call_print_bug.ml \ - generated/src/tests/ptests_config \ - generated/src/tests/test_config \ - generated/src/tests/hello/hello_test.c - mkdir -p $@ - cp generated/multiple/* $@ - cp generated/src/run_call_print_bug.ml $@/hello_run.ml.bug - echo "" >> $@/hello_run.ml.bug - cat generated/src/extend_run.ml >> $@/hello_run.ml.bug - mkdir -p $@/tests - cp generated/src/tests/ptests_config $@/tests/ptests_config - cp generated/src/tests/test_config $@/tests/test_config - mkdir -p $@/tests/hello - cp generated/src/tests/hello/hello_test.c $@/tests/hello/hello_test.c - -generated/with_doc: generated/empty \ - generated/src/help_msg.ml \ - generated/src/register.ml \ - generated/src/options_enabled.ml \ - generated/src/options_output_file.ml \ - generated/src/print.ml \ - generated/src/run_call_print.ml \ - generated/src/extend_run.ml \ - generated/src/help_msg.doc.ml \ - generated/src/register.doc.ml \ - generated/src/options_enabled.doc.ml \ - generated/src/options_output_file.doc.ml \ - generated/src/print.doc.ml \ - generated/src/run_call_print.doc.ml \ - generated/src/extend_run.doc.ml \ - generated/src/hello_options.doc.ml \ - generated/src/hello_print.doc.ml \ - generated/src/hello_run.doc.ml \ - generated/src/tests/hello/oracle/hello_test.err.oracle \ - generated/src/tests/hello/oracle/hello_test.res.oracle - mkdir -p $@ - cp generated/empty/* $@ - cp generated/src/hello_options.doc.ml $@/hello_options.ml - echo "" >> $@/hello_options.ml - cat generated/src/help_msg.doc.ml >> $@/hello_options.ml - cat generated/src/help_msg.ml >> $@/hello_options.ml - echo "" >> $@/hello_options.ml - cat generated/src/register.doc.ml >> $@/hello_options.ml - cat generated/src/register.ml >> $@/hello_options.ml - echo "" >> $@/hello_options.ml - cat generated/src/options_enabled.doc.ml >> $@/hello_options.ml - cat generated/src/options_enabled.ml >> $@/hello_options.ml - echo "" >> $@/hello_options.ml - cat generated/src/options_output_file.doc.ml >> $@/hello_options.ml - cat generated/src/options_output_file.ml >> $@/hello_options.ml - cp generated/src/hello_print.doc.ml $@/hello_print.ml - echo "" >> $@/hello_print.ml - cat generated/src/print.doc.ml >> $@/hello_print.ml - cat generated/src/print.ml >> $@/hello_print.ml - cp generated/src/hello_run.doc.ml $@/hello_run.ml - echo "" >> $@/hello_run.ml - cat generated/src/run_call_print.doc.ml >> $@/hello_run.ml - cat generated/src/run_call_print.ml >> $@/hello_run.ml - echo "" >> $@/hello_run.ml - cat generated/src/extend_run.doc.ml >> $@/hello_run.ml - cat generated/src/extend_run.ml >> $@/hello_run.ml - mkdir -p $@/tests/hello - cp generated/src/tests/hello/hello_test.c $@/tests/hello/hello_test.c - mkdir -p $@/tests/hello/oracle - cp generated/src/tests/hello/oracle/hello_test.err.oracle $@/tests/hello/oracle/hello_test.err.oracle - cp generated/src/tests/hello/oracle/hello_test.res.oracle $@/tests/hello/oracle/hello_test.res.oracle - -tests: - cd generated/script && frama-c -load-script hello_world.ml && cat hello.out - cd generated/with_registration && frama-c -load-script hello_world.ml && cat hello.out - cd generated/with_log && frama-c -load-script hello_world.ml -hello-verbose 2 - cd generated/with_options && make && frama-c -load-module ./top/Hello - cd generated/makefile_single && make && frama-c -load-module ./top/Hello - cd generated/makefile_multiple && make && frama-c -load-module ./top/Hello - cd generated/with_test && make && frama-c -load-module ./top/Hello - cd generated/with_doc && make && frama-c -load-module ./top/Hello - -clean: - rm -Rf generated -- GitLab