Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/C/Linux/tools/verification/rvgen/rvgen/templates/dot2k/   (Open Source Betriebssystem Version 6.17.9©)  Datei vom 24.10.2025 mit Größe 1 kB image not shown  

Quelle  main.c   Sprache: C

 
// SPDX-License-Identifier: GPL-2.0
#include <linux/ftrace.h>
#include <linux/tracepoint.h>
#include <linux/kernel.h>
#include <linux/module.h>
#include <linux/init.h>
#include <linux/rv.h>
#include <rv/instrumentation.h>
#include <rv/da_monitor.h>

#define MODULE_NAME "%%MODEL_NAME%%"

/*
 * XXX: include required tracepoint headers, e.g.,
 * #include <trace/events/sched.h>
 */

#include <rv_trace.h>
%%INCLUDE_PARENT%%
/*
 * This is the self-generated part of the monitor. Generally, there is no need
 * to touch this section.
 */

#include "%%MODEL_NAME%%.h"

/*
 * Declare the deterministic automata monitor.
 *
 * The rv monitor reference is needed for the monitor declaration.
 */

static struct rv_monitor rv_%%MODEL_NAME%%;
DECLARE_DA_MON_%%MONITOR_TYPE%%(%%MODEL_NAME%%, %%MIN_TYPE%%);

/*
 * This is the instrumentation part of the monitor.
 *
 * This is the section where manual work is required. Here the kernel events
 * are translated into model's event.
 *
 */

%%TRACEPOINT_HANDLERS_SKEL%%
static int enable_%%MODEL_NAME%%(void)
{
 int retval;

 retval = da_monitor_init_%%MODEL_NAME%%();
 if (retval)
  return retval;

%%TRACEPOINT_ATTACH%%

 return 0;
}

static void disable_%%MODEL_NAME%%(void)
{
 rv_%%MODEL_NAME%%.enabled = 0;

%%TRACEPOINT_DETACH%%

 da_monitor_destroy_%%MODEL_NAME%%();
}

/*
 * This is the monitor register section.
 */

static struct rv_monitor rv_%%MODEL_NAME%% = {
 .name = "%%MODEL_NAME%%",
 .description = "%%DESCRIPTION%%",
 .enable = enable_%%MODEL_NAME%%,
 .disable = disable_%%MODEL_NAME%%,
 .reset = da_monitor_reset_all_%%MODEL_NAME%%,
 .enabled = 0,
};

static int __init register_%%MODEL_NAME%%(void)
{
 return rv_register_monitor(&rv_%%MODEL_NAME%%, %%PARENT%%);
}

static void __exit unregister_%%MODEL_NAME%%(void)
{
 rv_unregister_monitor(&rv_%%MODEL_NAME%%);
}

module_init(register_%%MODEL_NAME%%);
module_exit(unregister_%%MODEL_NAME%%);

MODULE_LICENSE("GPL");
MODULE_AUTHOR("dot2k: auto-generated");
MODULE_DESCRIPTION("%%MODEL_NAME%%: %%DESCRIPTION%%");

Messung V0.5
C=91 H=91 G=90

¤ Dauer der Verarbeitung: 0.2 Sekunden  ¤

*© Formatika GbR, Deutschland






Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.